We will prove Hausdorff_space R R_standard_topology.
We will prove topology_on R R_standard_topology ∧ ∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
Let x1 and x2 be given.
Assume Hx1R: x1 ∈ R.
Assume Hx2R: x2 ∈ R.
Assume Hneq: x1 ≠ x2.
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1R).
We prove the intermediate claim Hx2S: SNo x2.
An exact proof term for the current goal is (real_SNo x2 Hx2R).
Apply (SNoLt_trichotomy_or_impred x1 x2 Hx1S Hx2S (∃U V : set, U ∈ R_standard_topology ∧ V ∈ R_standard_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.
Assume Hlt12: x1 < x2.
We prove the intermediate claim Hx1x2: Rlt x1 x2.
An exact proof term for the current goal is (RltI x1 x2 Hx1R Hx2R Hlt12).
Apply (rational_dense_between_reals x1 x2 Hx1R Hx2R Hx1x2) to the current goal.
Let q be given.
Assume Hqcore.
Apply Hqcore to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqconj: Rlt x1 q ∧ Rlt q x2.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
Set U to be the term {x ∈ R|Rlt x q}.
Set V to be the term {x ∈ R|Rlt q x}.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We prove the intermediate claim HUopen: U ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology q HqR).
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology q HqR).
We prove the intermediate claim Hx1ltq: Rlt x1 q.
An exact proof term for the current goal is (andEL (Rlt x1 q) (Rlt q x2) Hqconj).
We prove the intermediate claim Hqltx2: Rlt q x2.
An exact proof term for the current goal is (andER (Rlt x1 q) (Rlt q x2) Hqconj).
We prove the intermediate claim Hx1U: x1 ∈ U.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 q) x1 Hx1R Hx1ltq).
We prove the intermediate claim Hx2V: x2 ∈ V.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt q x0) x2 Hx2R Hqltx2).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∩ V.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x HxUV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x HxUV).
We prove the intermediate claim Hxltq: Rlt x q.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 q) x HxU).
We prove the intermediate claim Hqltx: Rlt q x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt q x0) x HxV).
We prove the intermediate claim Hqq: Rlt q q.
An exact proof term for the current goal is (Rlt_tra q x q Hqltx Hxltq).
An exact proof term for the current goal is ((not_Rlt_refl q HqR) Hqq).
Apply andI to the current goal.
We will prove ((U ∈ R_standard_topology ∧ V ∈ R_standard_topology) ∧ x1 ∈ U) ∧ x2 ∈ V.
Apply andI to the current goal.
We will prove (U ∈ R_standard_topology ∧ V ∈ R_standard_topology) ∧ x1 ∈ U.
Apply andI to the current goal.
We will prove U ∈ R_standard_topology ∧ V ∈ R_standard_topology.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is Hx1U.
An exact proof term for the current goal is Hx2V.
An exact proof term for the current goal is HUVempty.
Assume Heq: x1 = x2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Heq).
Assume Hlt21: x2 < x1.
We prove the intermediate claim Hx2x1: Rlt x2 x1.
An exact proof term for the current goal is (RltI x2 x1 Hx2R Hx1R Hlt21).
Apply (rational_dense_between_reals x2 x1 Hx2R Hx1R Hx2x1) to the current goal.
Let q be given.
Assume Hqcore.
Apply Hqcore to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume Hqconj: Rlt x2 q ∧ Rlt q x1.
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
Set U to be the term {x ∈ R|Rlt q x}.
Set V to be the term {x ∈ R|Rlt x q}.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We prove the intermediate claim HUopen: U ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology q HqR).
We prove the intermediate claim HVopen: V ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology q HqR).
We prove the intermediate claim Hqltx1: Rlt q x1.
An exact proof term for the current goal is (andER (Rlt x2 q) (Rlt q x1) Hqconj).
We prove the intermediate claim Hx2ltq: Rlt x2 q.
An exact proof term for the current goal is (andEL (Rlt x2 q) (Rlt q x1) Hqconj).
We prove the intermediate claim Hx1U: x1 ∈ U.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt q x0) x1 Hx1R Hqltx1).
We prove the intermediate claim Hx2V: x2 ∈ V.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 q) x2 Hx2R Hx2ltq).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∩ V.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x HxUV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x HxUV).
We prove the intermediate claim Hqltx: Rlt q x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt q x0) x HxU).
We prove the intermediate claim Hxltq: Rlt x q.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 q) x HxV).
We prove the intermediate claim Hqq: Rlt q q.
An exact proof term for the current goal is (Rlt_tra q x q Hqltx Hxltq).
An exact proof term for the current goal is ((not_Rlt_refl q HqR) Hqq).
Apply andI to the current goal.
We will prove ((U ∈ R_standard_topology ∧ V ∈ R_standard_topology) ∧ x1 ∈ U) ∧ x2 ∈ V.
Apply andI to the current goal.
We will prove (U ∈ R_standard_topology ∧ V ∈ R_standard_topology) ∧ x1 ∈ U.
Apply andI to the current goal.
We will prove U ∈ R_standard_topology ∧ V ∈ R_standard_topology.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is Hx1U.
An exact proof term for the current goal is Hx2V.
An exact proof term for the current goal is HUVempty.
∎