We will prove dense_in rational_numbers Sorgenfrey_line Sorgenfrey_topology.
We will prove closure_of Sorgenfrey_line Sorgenfrey_topology rational_numbers = Sorgenfrey_line.
Apply set_ext to the current goal.
An exact proof term for the current goal is (closure_in_space Sorgenfrey_line Sorgenfrey_topology rational_numbers R_lower_limit_topology_is_topology).
Let x be given.
Assume HxR: x ∈ Sorgenfrey_line.
We will prove x ∈ closure_of Sorgenfrey_line Sorgenfrey_topology rational_numbers.
We prove the intermediate claim Hcliff: x ∈ closure_of Sorgenfrey_line Sorgenfrey_topology rational_numbers ↔ (∀U ∈ Sorgenfrey_topology, x ∈ U → U ∩ rational_numbers ≠ Empty).
An exact proof term for the current goal is (closure_characterization Sorgenfrey_line Sorgenfrey_topology rational_numbers x R_lower_limit_topology_is_topology HxR).
Apply (iffER (x ∈ closure_of Sorgenfrey_line Sorgenfrey_topology rational_numbers) (∀U ∈ Sorgenfrey_topology, x ∈ U → U ∩ rational_numbers ≠ Empty) Hcliff) to the current goal.
We will prove ∀U ∈ Sorgenfrey_topology, x ∈ U → U ∩ rational_numbers ≠ Empty.
Let U be given.
Assume HU: U ∈ Sorgenfrey_topology.
Assume HxU: x ∈ U.
We prove the intermediate claim HTdef: Sorgenfrey_topology = generated_topology R R_lower_limit_basis.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology R R_lower_limit_basis.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HU.
We prove the intermediate claim Hloc: ∀y0 ∈ U, ∃b0 ∈ R_lower_limit_basis, y0 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀y1 ∈ U0, ∃b0 ∈ R_lower_limit_basis, y1 ∈ b0 ∧ b0 ⊆ U0) U HUgen).
We prove the intermediate claim Hexb0: ∃b0 ∈ R_lower_limit_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (Hloc x HxU).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
Apply Hb0pair to the current goal.
Assume Hb0B: b0 ∈ R_lower_limit_basis.
Assume Hb0prop: x ∈ b0 ∧ b0 ⊆ U.
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hexa: ∃a ∈ R, b0 ∈ {halfopen_interval_left a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) b0 Hb0B).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
Apply Hapair to the current goal.
Assume HaR: a ∈ R.
Assume Hb0fam: b0 ∈ {halfopen_interval_left a b|b ∈ R}.
We prove the intermediate claim Hexb: ∃b ∈ R, b0 = halfopen_interval_left a b.
An exact proof term for the current goal is (ReplE R (λb1 : set ⇒ halfopen_interval_left a b1) b0 Hb0fam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbR: b ∈ R.
Assume Hb0eq: b0 = halfopen_interval_left a b.
We prove the intermediate claim HxIn: x ∈ halfopen_interval_left a b.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxProp: ¬ (Rlt x a) ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) x HxIn).
We prove the intermediate claim Hnltxa: ¬ (Rlt x a).
An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (Rlt x b) HxProp).
We prove the intermediate claim Hxltb: Rlt x b.
An exact proof term for the current goal is (andER (¬ (Rlt x a)) (Rlt x b) HxProp).
We prove the intermediate claim Hax: Rle a x.
An exact proof term for the current goal is (RleI a x HaR HxR Hnltxa).
We prove the intermediate claim Hab: Rlt a b.
An exact proof term for the current goal is (Rle_Rlt_tra a x b Hax Hxltb).
Apply (rational_dense_between_reals a b HaR HbR Hab) 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 a q ∧ Rlt q b) Hqpair).
We prove the intermediate claim HqProp: Rlt a q ∧ Rlt q b.
An exact proof term for the current goal is (andER (q ∈ rational_numbers) (Rlt a q ∧ Rlt q b) Hqpair).
We prove the intermediate claim Haq: Rlt a q.
An exact proof term for the current goal is (andEL (Rlt a q) (Rlt q b) HqProp).
We prove the intermediate claim Hqb: Rlt q b.
An exact proof term for the current goal is (andER (Rlt a q) (Rlt q b) 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 Hnltqa: ¬ (Rlt q a).
An exact proof term for the current goal is (not_Rlt_sym a q Haq).
We prove the intermediate claim HqInb0: q ∈ halfopen_interval_left a b.
An exact proof term for the current goal is (SepI R (λz0 : set ⇒ ¬ (Rlt z0 a) ∧ Rlt z0 b) q HqR (andI (¬ (Rlt q a)) (Rlt q b) Hnltqa Hqb)).
We prove the intermediate claim HqInU: q ∈ U.
We prove the intermediate claim HqInb0': q ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HqInb0.
An exact proof term for the current goal is (Hb0subU q HqInb0').
We will prove U ∩ rational_numbers ≠ Empty.
Assume HUQ: U ∩ rational_numbers = Empty.
We prove the intermediate claim HqUA: q ∈ U ∩ rational_numbers.
An exact proof term for the current goal is (binintersectI U rational_numbers q HqInU HqQ).
We prove the intermediate claim HqEmp: q ∈ Empty.
rewrite the current goal using HUQ (from right to left).
An exact proof term for the current goal is HqUA.
An exact proof term for the current goal is (EmptyE q HqEmp False).
∎