Let U0 be given.
Assume HU0Tx: U0 ∈ unit_interval_topology.
Assume HepsU0: eps_ 1 ∈ U0.
We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
We prove the intermediate claim HU0Sub: U0 ∈ subspace_topology R R_standard_topology unit_interval.
rewrite the current goal using Hut (from right to left).
An exact proof term for the current goal is HU0Tx.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (SepE1 (𝒫 unit_interval) (λU : set ⇒ ∃V ∈ R_standard_topology, U = V ∩ unit_interval) U0 HU0Sub).
We prove the intermediate claim HU0subI: U0 ⊆ unit_interval.
An exact proof term for the current goal is (PowerE unit_interval U0 HU0Pow).
We prove the intermediate claim HepsI: eps_ 1 ∈ unit_interval.
An exact proof term for the current goal is (HU0subI (eps_ 1) HepsU0).
We prove the intermediate claim HepsR: eps_ 1 ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R (eps_ 1) HepsI).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim HepsS: SNo (eps_ 1).
An exact proof term for the current goal is (real_SNo (eps_ 1) HepsR).
We prove the intermediate claim HepsPosS: 0 < (eps_ 1).
An exact proof term for the current goal is (SNo_eps_pos 1 H1omega).
We prove the intermediate claim H0ltEps: Rlt 0 (eps_ 1).
An exact proof term for the current goal is (RltI 0 (eps_ 1) real_0 HepsR HepsPosS).
We prove the intermediate claim H0Ord: ordinal 0.
An exact proof term for the current goal is (nat_p_ordinal 0 nat_0).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is (ordinal_0_In_ordsucc 0 H0Ord).
We prove the intermediate claim HepsLt1S: (eps_ 1) < 1.
We prove the intermediate claim HepsLtE0: eps_ 1 < eps_ 0.
An exact proof term for the current goal is (SNo_eps_decr 1 H1omega 0 H0in1).
rewrite the current goal using (eps_0_1) (from right to left) at position 2.
An exact proof term for the current goal is HepsLtE0.
We prove the intermediate claim HepsLt1: Rlt (eps_ 1) 1.
An exact proof term for the current goal is (RltI (eps_ 1) 1 HepsR real_1 HepsLt1S).
We prove the intermediate claim HexV: ∃V ∈ R_standard_topology, U0 = V ∩ unit_interval.
An exact proof term for the current goal is (SepE2 (𝒫 unit_interval) (λU : set ⇒ ∃V ∈ R_standard_topology, U = V ∩ unit_interval) U0 HU0Sub).
Apply HexV to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HV: V ∈ R_standard_topology.
An exact proof term for the current goal is (andEL (V ∈ R_standard_topology) (U0 = V ∩ unit_interval) HVpair).
We prove the intermediate claim HU0eq: U0 = V ∩ unit_interval.
An exact proof term for the current goal is (andER (V ∈ R_standard_topology) (U0 = V ∩ unit_interval) HVpair).
We prove the intermediate claim HepsV: eps_ 1 ∈ V.
We prove the intermediate claim HepsCap: eps_ 1 ∈ V ∩ unit_interval.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HepsU0.
Apply (binintersectE V unit_interval (eps_ 1) HepsCap) to the current goal.
Assume HepsV0 HepsI0.
An exact proof term for the current goal is HepsV0.
We prove the intermediate claim HrTopDef: R_standard_topology = generated_topology R R_standard_basis.
Use reflexivity.
We prove the intermediate claim HVgen: V ∈ generated_topology R R_standard_basis.
rewrite the current goal using HrTopDef (from right to left).
An exact proof term for the current goal is HV.
We prove the intermediate claim HVprop: ∀x ∈ V, ∃b ∈ R_standard_basis, x ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU : set ⇒ ∀x0 ∈ U, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U) V HVgen).
We prove the intermediate claim Hexb: ∃b ∈ R_standard_basis, eps_ 1 ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (HVprop (eps_ 1) HepsV).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (b ∈ R_standard_basis) (eps_ 1 ∈ b ∧ b ⊆ V) Hbpair).
We prove the intermediate claim Hbprop: eps_ 1 ∈ b ∧ b ⊆ V.
An exact proof term for the current goal is (andER (b ∈ R_standard_basis) (eps_ 1 ∈ b ∧ b ⊆ V) Hbpair).
We prove the intermediate claim Hepsb: eps_ 1 ∈ b.
An exact proof term for the current goal is (andEL (eps_ 1 ∈ b) (b ⊆ V) Hbprop).
We prove the intermediate claim HbsubV: b ⊆ V.
An exact proof term for the current goal is (andER (eps_ 1 ∈ b) (b ⊆ V) Hbprop).
We prove the intermediate claim Hexa: ∃a ∈ R, b ∈ {open_interval a bb|bb ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 bb|bb ∈ R}) b HbB).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (b ∈ {open_interval a bb|bb ∈ R}) Hapair).
We prove the intermediate claim HbFam: b ∈ {open_interval a bb|bb ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (b ∈ {open_interval a bb|bb ∈ R}) Hapair).
We prove the intermediate claim Hexbb: ∃bb ∈ R, b = open_interval a bb.
An exact proof term for the current goal is (ReplE R (λbb0 : set ⇒ open_interval a bb0) b HbFam).
Apply Hexbb to the current goal.
Let bb be given.
Assume Hbbpair.
We prove the intermediate claim HbbR: bb ∈ R.
An exact proof term for the current goal is (andEL (bb ∈ R) (b = open_interval a bb) Hbbpair).
We prove the intermediate claim Hbeq: b = open_interval a bb.
An exact proof term for the current goal is (andER (bb ∈ R) (b = open_interval a bb) Hbbpair).
We prove the intermediate claim HepsInInt: eps_ 1 ∈ open_interval a bb.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hepsb.
We prove the intermediate claim HepsIntProp: Rlt a (eps_ 1) ∧ Rlt (eps_ 1) bb.
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ Rlt a t ∧ Rlt t bb) (eps_ 1) HepsInInt).
We prove the intermediate claim HaLtEps: Rlt a (eps_ 1).
An exact proof term for the current goal is (andEL (Rlt a (eps_ 1)) (Rlt (eps_ 1) bb) HepsIntProp).
We prove the intermediate claim HepsLtbb: Rlt (eps_ 1) bb.
An exact proof term for the current goal is (andER (Rlt a (eps_ 1)) (Rlt (eps_ 1) bb) HepsIntProp).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbbS: SNo bb.
An exact proof term for the current goal is (real_SNo bb HbbR).
Apply (SNoLt_trichotomy_or_impred bb 1 HbbS SNo_1 (∃x : set, x ∈ U0 ∧ x ≠ eps_ 1)) to the current goal.
Assume HbbLt1S: bb < 1.
We prove the intermediate claim HbbLt1: Rlt bb 1.
An exact proof term for the current goal is (RltI bb 1 HbbR real_1 HbbLt1S).
Apply (rational_dense_between_reals (eps_ 1) bb HepsR HbbR HepsLtbb) to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q bb) Hqpair).
We prove the intermediate claim Hqprop: Rlt (eps_ 1) q ∧ Rlt q bb.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q bb) Hqpair).
We prove the intermediate claim HepsLtq: Rlt (eps_ 1) q.
An exact proof term for the current goal is (andEL (Rlt (eps_ 1) q) (Rlt q bb) Hqprop).
We prove the intermediate claim HqLtbb: Rlt q bb.
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q bb) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HaLtq: Rlt a q.
An exact proof term for the current goal is (Rlt_tra a (eps_ 1) q HaLtEps HepsLtq).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: Rlt a q ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is HaLtq.
An exact proof term for the current goal is HqLtbb.
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt a t ∧ Rlt t bb) q HqR Hqconj).
We prove the intermediate claim HqInV: q ∈ V.
An exact proof term for the current goal is (HbsubV q HqInb).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q H0ltEps HepsLtq).
We prove the intermediate claim HqLt1: Rlt q 1.
An exact proof term for the current goal is (Rlt_tra q bb 1 HqLtbb HbbLt1).
We prove the intermediate claim Hnltq0: ¬ (Rlt q 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
We prove the intermediate claim Hnlt1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 HqLt1).
We prove the intermediate claim HqInI: q ∈ unit_interval.
We prove the intermediate claim Hqconj: ¬ (Rlt q 0) ∧ ¬ (Rlt 1 q).
Apply andI to the current goal.
An exact proof term for the current goal is Hnltq0.
An exact proof term for the current goal is Hnlt1q.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) q HqR Hqconj).
We prove the intermediate claim HqInU0: q ∈ U0.
rewrite the current goal using HU0eq (from left to right).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HqInV.
An exact proof term for the current goal is HqInI.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HqInU0.
We will prove q ≠ eps_ 1.
Assume Heq: q = eps_ 1.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HepsLtq.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) HepsR) Hbad).
Assume HbbEq: bb = 1.
Apply (rational_dense_between_reals (eps_ 1) 1 HepsR real_1 HepsLt1) to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q 1) Hqpair).
We prove the intermediate claim Hqprop: Rlt (eps_ 1) q ∧ Rlt q 1.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q 1) Hqpair).
We prove the intermediate claim HepsLtq: Rlt (eps_ 1) q.
An exact proof term for the current goal is (andEL (Rlt (eps_ 1) q) (Rlt q 1) Hqprop).
We prove the intermediate claim HqLt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q 1) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HaLtq: Rlt a q.
An exact proof term for the current goal is (Rlt_tra a (eps_ 1) q HaLtEps HepsLtq).
We prove the intermediate claim HqLtbb: Rlt q bb.
rewrite the current goal using HbbEq (from left to right).
An exact proof term for the current goal is HqLt1.
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: Rlt a q ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is HaLtq.
An exact proof term for the current goal is HqLtbb.
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt a t ∧ Rlt t bb) q HqR Hqconj).
We prove the intermediate claim HqInV: q ∈ V.
An exact proof term for the current goal is (HbsubV q HqInb).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q H0ltEps HepsLtq).
We prove the intermediate claim Hnltq0: ¬ (Rlt q 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
We prove the intermediate claim Hnlt1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 HqLt1).
We prove the intermediate claim HqInI: q ∈ unit_interval.
We prove the intermediate claim Hqconj: ¬ (Rlt q 0) ∧ ¬ (Rlt 1 q).
Apply andI to the current goal.
An exact proof term for the current goal is Hnltq0.
An exact proof term for the current goal is Hnlt1q.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) q HqR Hqconj).
We prove the intermediate claim HqInU0: q ∈ U0.
rewrite the current goal using HU0eq (from left to right).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HqInV.
An exact proof term for the current goal is HqInI.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HqInU0.
We will prove q ≠ eps_ 1.
Assume Heq: q = eps_ 1.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HepsLtq.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) HepsR) Hbad).
Assume H1LtbbS: 1 < bb.
We prove the intermediate claim H1Ltbb: Rlt 1 bb.
An exact proof term for the current goal is (RltI 1 bb real_1 HbbR H1LtbbS).
Apply (rational_dense_between_reals (eps_ 1) 1 HepsR real_1 HepsLt1) to the current goal.
Let q be given.
Assume Hqpair.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (andEL (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q 1) Hqpair).
We prove the intermediate claim Hqprop: Rlt (eps_ 1) q ∧ Rlt q 1.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt (eps_ 1) q ∧ Rlt q 1) Hqpair).
We prove the intermediate claim HepsLtq: Rlt (eps_ 1) q.
An exact proof term for the current goal is (andEL (Rlt (eps_ 1) q) (Rlt q 1) Hqprop).
We prove the intermediate claim HqLt1: Rlt q 1.
An exact proof term for the current goal is (andER (Rlt (eps_ 1) q) (Rlt q 1) Hqprop).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HaLtq: Rlt a q.
An exact proof term for the current goal is (Rlt_tra a (eps_ 1) q HaLtEps HepsLtq).
We prove the intermediate claim HqLtbb: Rlt q bb.
An exact proof term for the current goal is (Rlt_tra q 1 bb HqLt1 H1Ltbb).
We prove the intermediate claim HqInb: q ∈ b.
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hqconj: Rlt a q ∧ Rlt q bb.
Apply andI to the current goal.
An exact proof term for the current goal is HaLtq.
An exact proof term for the current goal is HqLtbb.
An exact proof term for the current goal is (SepI R (λt : set ⇒ Rlt a t ∧ Rlt t bb) q HqR Hqconj).
We prove the intermediate claim HqInV: q ∈ V.
An exact proof term for the current goal is (HbsubV q HqInb).
We prove the intermediate claim H0ltq: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 (eps_ 1) q H0ltEps HepsLtq).
We prove the intermediate claim Hnltq0: ¬ (Rlt q 0).
An exact proof term for the current goal is (not_Rlt_sym 0 q H0ltq).
We prove the intermediate claim Hnlt1q: ¬ (Rlt 1 q).
An exact proof term for the current goal is (not_Rlt_sym q 1 HqLt1).
We prove the intermediate claim HqInI: q ∈ unit_interval.
We prove the intermediate claim Hqconj: ¬ (Rlt q 0) ∧ ¬ (Rlt 1 q).
Apply andI to the current goal.
An exact proof term for the current goal is Hnltq0.
An exact proof term for the current goal is Hnlt1q.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) q HqR Hqconj).
We prove the intermediate claim HqInU0: q ∈ U0.
rewrite the current goal using HU0eq (from left to right).
Apply binintersectI to the current goal.
An exact proof term for the current goal is HqInV.
An exact proof term for the current goal is HqInI.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HqInU0.
We will prove q ≠ eps_ 1.
Assume Heq: q = eps_ 1.
We prove the intermediate claim Hbad: Rlt (eps_ 1) (eps_ 1).
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HepsLtq.
An exact proof term for the current goal is ((not_Rlt_refl (eps_ 1) HepsR) Hbad).
∎