We will prove component_of R R_lower_limit_topology 0 = {0} ∧ (∀x : set, x ∈ R → component_of R R_lower_limit_topology x = {x}).
We prove the intermediate claim Hall: ∀x : set, x ∈ R → component_of R R_lower_limit_topology x = {x}.
Let x be given.
Assume HxR: x ∈ R.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ component_of R R_lower_limit_topology x.
We will prove y ∈ {x}.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyR).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim HyProp: ∃C : set, connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C ∧ y ∈ C.
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C ∧ y0 ∈ C) y Hy).
Apply (SNoLt_trichotomy_or_impred y x HyS HxS (y ∈ {x})) to the current goal.
Assume Hylt: y < x.
Apply HyProp to the current goal.
Let C be given.
Assume HC.
We prove the intermediate claim HCcore: connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C.
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HCconn: connected_space C (subspace_topology R R_lower_limit_topology C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology R R_lower_limit_topology C)) (x ∈ C) HCcore).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology R R_lower_limit_topology C)) (x ∈ C) HCcore).
We prove the intermediate claim HTl: topology_on R R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HCsubR: C ⊆ R.
An exact proof term for the current goal is (connected_subspace_subset R R_lower_limit_topology C HTl HCconn).
Set I to be the term halfopen_interval_left y x.
We prove the intermediate claim Hyx: Rlt y x.
An exact proof term for the current goal is (RltI y x HyR HxR Hylt).
We prove the intermediate claim HI: I ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology y x HyR HxR).
We prove the intermediate claim HcompI: (R ∖ I) ∈ R_lower_limit_topology.
An exact proof term for the current goal is (complement_halfopen_interval_left_in_R_lower_limit_topology y x HyR HxR).
Set A to be the term I ∩ C.
We prove the intermediate claim HAne: A ≠ Empty.
Assume Heq: A = Empty.
We prove the intermediate claim HyI: y ∈ I.
An exact proof term for the current goal is (halfopen_interval_left_leftmem y x Hyx).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectI I C y HyI HyC).
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is (EmptyE y HyE).
We prove the intermediate claim HAnC: A ≠ C.
Assume Heq: A = C.
We prove the intermediate claim HxNotI: x ∉ I.
Assume HxinI: x ∈ I.
We prove the intermediate claim HxPropI: ¬ (Rlt x y) ∧ Rlt x x.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z y) ∧ Rlt z x) x HxinI).
We prove the intermediate claim HxSelf: Rlt x x.
An exact proof term for the current goal is (andER (¬ (Rlt x y)) (Rlt x x) HxPropI).
An exact proof term for the current goal is ((not_Rlt_refl x HxR) HxSelf).
We prove the intermediate claim HxNotA: x ∉ A.
Assume HxA: x ∈ A.
An exact proof term for the current goal is (HxNotI (binintersectE1 I C x HxA)).
We prove the intermediate claim HxA': x ∈ A.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HxC.
An exact proof term for the current goal is (HxNotA HxA').
Set Tc to be the term subspace_topology R R_lower_limit_topology C.
We prove the intermediate claim HTc: topology_on C Tc.
An exact proof term for the current goal is (andEL (topology_on C Tc) (¬ (∃U V : set, U ∈ Tc ∧ V ∈ Tc ∧ separation_of C U V)) HCconn).
We prove the intermediate claim HAinTc: A ∈ Tc.
An exact proof term for the current goal is (subspace_topologyI R R_lower_limit_topology C I HI).
We prove the intermediate claim HAopen: open_in C Tc A.
An exact proof term for the current goal is (andI (topology_on C Tc) (A ∈ Tc) HTc HAinTc).
We prove the intermediate claim HUinTc: (C ∖ A) ∈ Tc.
We prove the intermediate claim HeqU: C ∖ A = (R ∖ I) ∩ C.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ C ∖ A.
We will prove z ∈ (R ∖ I) ∩ C.
We prove the intermediate claim Hzpair: z ∈ C ∧ z ∉ A.
An exact proof term for the current goal is (setminusE C A z Hz).
We prove the intermediate claim HzC: z ∈ C.
An exact proof term for the current goal is (andEL (z ∈ C) (z ∉ A) Hzpair).
We prove the intermediate claim HzNotA: z ∉ A.
An exact proof term for the current goal is (andER (z ∈ C) (z ∉ A) Hzpair).
We prove the intermediate claim HzR: z ∈ R.
An exact proof term for the current goal is (HCsubR z HzC).
We prove the intermediate claim HzNotI: z ∉ I.
Assume HzI: z ∈ I.
Apply HzNotA to the current goal.
An exact proof term for the current goal is (binintersectI I C z HzI HzC).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (setminusI R I z HzR HzNotI).
An exact proof term for the current goal is HzC.
Let z be given.
Assume Hz: z ∈ (R ∖ I) ∩ C.
We will prove z ∈ C ∖ A.
Apply (binintersectE (R ∖ I) C z Hz) to the current goal.
Assume HzRI: z ∈ R ∖ I.
Assume HzC: z ∈ C.
We prove the intermediate claim HzNotI: z ∉ I.
An exact proof term for the current goal is (setminusE2 R I z HzRI).
Apply (setminusI C A z HzC) to the current goal.
Assume HzA: z ∈ A.
An exact proof term for the current goal is (HzNotI (binintersectE1 I C z HzA)).
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is (subspace_topologyI R R_lower_limit_topology C (R ∖ I) HcompI).
We prove the intermediate claim HAclosed: closed_in C Tc A.
rewrite the current goal using (setminus_setminus_eq C A (binintersect_Subq_2 I C)) (from right to left).
An exact proof term for the current goal is (closed_of_open_complement C Tc (C ∖ A) HTc HUinTc).
We prove the intermediate claim Hnoclopen: ¬ (∃A0 : set, A0 ≠ Empty ∧ A0 ≠ C ∧ open_in C Tc A0 ∧ closed_in C Tc A0).
An exact proof term for the current goal is (iffEL (connected_space C Tc) (¬ (∃A0 : set, A0 ≠ Empty ∧ A0 ≠ C ∧ open_in C Tc A0 ∧ closed_in C Tc A0)) (connected_iff_no_nontrivial_clopen C Tc HTc) HCconn).
Apply FalseE to the current goal.
Apply Hnoclopen to the current goal.
We use A to witness the existential quantifier.
We prove the intermediate claim Hpair: A ≠ Empty ∧ A ≠ C.
An exact proof term for the current goal is (andI (A ≠ Empty) (A ≠ C) HAne HAnC).
We prove the intermediate claim Htriple: (A ≠ Empty ∧ A ≠ C) ∧ open_in C Tc A.
An exact proof term for the current goal is (andI (A ≠ Empty ∧ A ≠ C) (open_in C Tc A) Hpair HAopen).
An exact proof term for the current goal is (andI ((A ≠ Empty ∧ A ≠ C) ∧ open_in C Tc A) (closed_in C Tc A) Htriple HAclosed).
Assume Hyeq: y = x.
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (SingI x).
Assume Hxlt: x < y.
Apply HyProp to the current goal.
Let C be given.
Assume HC.
We prove the intermediate claim HCcore: connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C.
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology R R_lower_limit_topology C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HCconn: connected_space C (subspace_topology R R_lower_limit_topology C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology R R_lower_limit_topology C)) (x ∈ C) HCcore).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology R R_lower_limit_topology C)) (x ∈ C) HCcore).
We prove the intermediate claim HTl: topology_on R R_lower_limit_topology.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
We prove the intermediate claim HCsubR: C ⊆ R.
An exact proof term for the current goal is (connected_subspace_subset R R_lower_limit_topology C HTl HCconn).
Set I to be the term halfopen_interval_left x y.
We prove the intermediate claim Hxylt: Rlt x y.
An exact proof term for the current goal is (RltI x y HxR HyR Hxlt).
We prove the intermediate claim HI: I ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x y HxR HyR).
We prove the intermediate claim HcompI: (R ∖ I) ∈ R_lower_limit_topology.
An exact proof term for the current goal is (complement_halfopen_interval_left_in_R_lower_limit_topology x y HxR HyR).
Set A to be the term I ∩ C.
We prove the intermediate claim HAne: A ≠ Empty.
Assume Heq: A = Empty.
We prove the intermediate claim HxI: x ∈ I.
An exact proof term for the current goal is (halfopen_interval_left_leftmem x y Hxylt).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectI I C x HxI HxC).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HxA.
An exact proof term for the current goal is (EmptyE x HxE).
We prove the intermediate claim HAnC: A ≠ C.
Assume Heq: A = C.
We prove the intermediate claim HyNotI: y ∉ I.
Assume HyinI: y ∈ I.
We prove the intermediate claim HyPropI: ¬ (Rlt y x) ∧ Rlt y y.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z y) y HyinI).
We prove the intermediate claim HySelf: Rlt y y.
An exact proof term for the current goal is (andER (¬ (Rlt y x)) (Rlt y y) HyPropI).
An exact proof term for the current goal is ((not_Rlt_refl y HyR) HySelf).
We prove the intermediate claim HyNotA: y ∉ A.
Assume HyA: y ∈ A.
An exact proof term for the current goal is (HyNotI (binintersectE1 I C y HyA)).
We prove the intermediate claim HyA': y ∈ A.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HyC.
An exact proof term for the current goal is (HyNotA HyA').
Set Tc to be the term subspace_topology R R_lower_limit_topology C.
We prove the intermediate claim HTc: topology_on C Tc.
An exact proof term for the current goal is (andEL (topology_on C Tc) (¬ (∃U V : set, U ∈ Tc ∧ V ∈ Tc ∧ separation_of C U V)) HCconn).
We prove the intermediate claim HAinTc: A ∈ Tc.
An exact proof term for the current goal is (subspace_topologyI R R_lower_limit_topology C I HI).
We prove the intermediate claim HAopen: open_in C Tc A.
An exact proof term for the current goal is (andI (topology_on C Tc) (A ∈ Tc) HTc HAinTc).
We prove the intermediate claim HUinTc: (C ∖ A) ∈ Tc.
We prove the intermediate claim HeqU: C ∖ A = (R ∖ I) ∩ C.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ C ∖ A.
We will prove z ∈ (R ∖ I) ∩ C.
We prove the intermediate claim Hzpair: z ∈ C ∧ z ∉ A.
An exact proof term for the current goal is (setminusE C A z Hz).
We prove the intermediate claim HzC: z ∈ C.
An exact proof term for the current goal is (andEL (z ∈ C) (z ∉ A) Hzpair).
We prove the intermediate claim HzNotA: z ∉ A.
An exact proof term for the current goal is (andER (z ∈ C) (z ∉ A) Hzpair).
We prove the intermediate claim HzR: z ∈ R.
An exact proof term for the current goal is (HCsubR z HzC).
We prove the intermediate claim HzNotI: z ∉ I.
Assume HzI: z ∈ I.
Apply HzNotA to the current goal.
An exact proof term for the current goal is (binintersectI I C z HzI HzC).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (setminusI R I z HzR HzNotI).
An exact proof term for the current goal is HzC.
Let z be given.
Assume Hz: z ∈ (R ∖ I) ∩ C.
We will prove z ∈ C ∖ A.
Apply (binintersectE (R ∖ I) C z Hz) to the current goal.
Assume HzRI: z ∈ R ∖ I.
Assume HzC: z ∈ C.
We prove the intermediate claim HzNotI: z ∉ I.
An exact proof term for the current goal is (setminusE2 R I z HzRI).
Apply (setminusI C A z HzC) to the current goal.
Assume HzA: z ∈ A.
An exact proof term for the current goal is (HzNotI (binintersectE1 I C z HzA)).
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is (subspace_topologyI R R_lower_limit_topology C (R ∖ I) HcompI).
We prove the intermediate claim HAclosed: closed_in C Tc A.
rewrite the current goal using (setminus_setminus_eq C A (binintersect_Subq_2 I C)) (from right to left).
An exact proof term for the current goal is (closed_of_open_complement C Tc (C ∖ A) HTc HUinTc).
We prove the intermediate claim Hnoclopen: ¬ (∃A0 : set, A0 ≠ Empty ∧ A0 ≠ C ∧ open_in C Tc A0 ∧ closed_in C Tc A0).
An exact proof term for the current goal is (iffEL (connected_space C Tc) (¬ (∃A0 : set, A0 ≠ Empty ∧ A0 ≠ C ∧ open_in C Tc A0 ∧ closed_in C Tc A0)) (connected_iff_no_nontrivial_clopen C Tc HTc) HCconn).
Apply FalseE to the current goal.
Apply Hnoclopen to the current goal.
We use A to witness the existential quantifier.
We prove the intermediate claim Hpair: A ≠ Empty ∧ A ≠ C.
An exact proof term for the current goal is (andI (A ≠ Empty) (A ≠ C) HAne HAnC).
We prove the intermediate claim Htriple: (A ≠ Empty ∧ A ≠ C) ∧ open_in C Tc A.
An exact proof term for the current goal is (andI (A ≠ Empty ∧ A ≠ C) (open_in C Tc A) Hpair HAopen).
An exact proof term for the current goal is (andI ((A ≠ Empty ∧ A ≠ C) ∧ open_in C Tc A) (closed_in C Tc A) Htriple HAclosed).
Let y be given.
Assume Hy: y ∈ {x}.
We will prove y ∈ component_of R R_lower_limit_topology x.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is (point_in_component R R_lower_limit_topology x R_lower_limit_topology_is_topology HxR).
Apply andI to the current goal.
An exact proof term for the current goal is (Hall 0 real_0).
An exact proof term for the current goal is Hall.
∎