Let X, Tx and m be given.
Assume Hloc: locally_m_euclidean X Tx m.
We will prove T1_space X Tx.
We prove the intermediate claim Hloc_parts: (m ∈ ω ∧ topology_on X Tx) ∧ (∀x0 : set, x0 ∈ X → ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0).
An exact proof term for the current goal is Hloc.
We prove the intermediate claim Htop: topology_on X Tx.
We prove the intermediate claim HmTop: m ∈ ω ∧ topology_on X Tx.
An exact proof term for the current goal is (andEL (m ∈ ω ∧ topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) Hloc_parts).
An exact proof term for the current goal is (andER (m ∈ ω) (topology_on X Tx) HmTop).
We prove the intermediate claim Hcharts: ∀x0 : set, x0 ∈ X → ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0.
An exact proof term for the current goal is (andER (m ∈ ω ∧ topology_on X Tx) (∀x0 : set, x0 ∈ X → ∃U0 : set, ∃V0 : set, ∃f0 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U0 (subspace_topology X Tx U0) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f0) Hloc_parts).
Apply (iffER (T1_space X Tx) (∀x0 : set, x0 ∈ X → closed_in X Tx {x0}) (lemma_T1_singletons_closed X Tx Htop)) to the current goal.
We will prove ∀x0 : set, x0 ∈ X → closed_in X Tx {x0}.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove closed_in X Tx {x0}.
We prove the intermediate claim HsingSub: {x0} ⊆ X.
Let y be given.
Assume Hy: y ∈ {x0}.
We prove the intermediate claim Hyeq: y = x0.
An exact proof term for the current goal is (SingE x0 y Hy).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is Hx0X.
We prove the intermediate claim Hsep_x0: ∀y : set, y ∈ X → y ≠ x0 → ∃W : set, W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W.
Let y be given.
Assume HyX: y ∈ X.
Assume Hyneq: y ≠ x0.
Apply (Hcharts y HyX) to the current goal.
Let U be given.
Assume HexVf.
Apply HexVf to the current goal.
Let V be given.
Assume Hexf.
Apply Hexf to the current goal.
Let f be given.
Assume Hprops.
We prove the intermediate claim Hleft: (((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V).
An exact proof term for the current goal is (andEL ((((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hprops).
We prove the intermediate claim Hhomeo: homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is (andER ((((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V)) (homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) Hprops).
We prove the intermediate claim Hmid: ((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)).
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft).
We prove the intermediate claim HVopen: open_in (euclidean_space m) (euclidean_topology m) V.
An exact proof term for the current goal is (andER ((open_in X Tx U ∧ y ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft).
We prove the intermediate claim Hpair: open_in X Tx U ∧ y ∈ U.
An exact proof term for the current goal is (andEL (open_in X Tx U ∧ y ∈ U) (V ⊆ (euclidean_space m)) Hmid).
We prove the intermediate claim HVsub: V ⊆ (euclidean_space m).
An exact proof term for the current goal is (andER (open_in X Tx U ∧ y ∈ U) (V ⊆ (euclidean_space m)) Hmid).
We prove the intermediate claim HUopen: open_in X Tx U.
An exact proof term for the current goal is (andEL (open_in X Tx U) (y ∈ U) Hpair).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (andER (open_in X Tx U) (y ∈ U) Hpair).
Apply (xm (x0 ∈ U)) to the current goal.
Assume Hx0U: x0 ∈ U.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HUopen).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (open_in_subset X Tx U HUopen).
We prove the intermediate claim HTU: topology_on U (subspace_topology X Tx U).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx U Htop HUsubX).
We prove the intermediate claim Hcontf: continuous_map U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
An exact proof term for the current goal is (andEL (continuous_map U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) (∃g : set, continuous_map V (subspace_topology (euclidean_space m) (euclidean_topology m) V) U (subspace_topology X Tx U) g ∧ (∀u : set, u ∈ U → apply_fun g (apply_fun f u) = u) ∧ (∀v : set, v ∈ V → apply_fun f (apply_fun g v) = v)) Hhomeo).
We prove the intermediate claim Hfunf: function_on f U V.
We prove the intermediate claim Htmp: (topology_on U (subspace_topology X Tx U) ∧ topology_on V (subspace_topology (euclidean_space m) (euclidean_topology m) V)) ∧ function_on f U V.
An exact proof term for the current goal is (andEL ((topology_on U (subspace_topology X Tx U) ∧ topology_on V (subspace_topology (euclidean_space m) (euclidean_topology m) V)) ∧ function_on f U V) (∀V1 : set, V1 ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V → preimage_of U f V1 ∈ subspace_topology X Tx U) Hcontf).
An exact proof term for the current goal is (andER (topology_on U (subspace_topology X Tx U) ∧ topology_on V (subspace_topology (euclidean_space m) (euclidean_topology m) V)) (function_on f U V) Htmp).
We prove the intermediate claim Hfx0V: apply_fun f x0 ∈ V.
An exact proof term for the current goal is (Hfunf x0 Hx0U).
We prove the intermediate claim HfyV: apply_fun f y ∈ V.
An exact proof term for the current goal is (Hfunf y HyU).
We prove the intermediate claim HT1E: T1_space (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (euclidean_space_T1 m).
We prove the intermediate claim HT1V: T1_space V (subspace_topology (euclidean_space m) (euclidean_topology m) V).
We prove the intermediate claim HtopE: topology_on (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (andEL (topology_on (euclidean_space m) (euclidean_topology m)) (∀F : set, F ⊆ euclidean_space m → finite F → closed_in (euclidean_space m) (euclidean_topology m) F) HT1E).
An exact proof term for the current goal is (subspace_T1 (euclidean_space m) (euclidean_topology m) V HtopE HVsub HT1E).
We prove the intermediate claim Hinj: ∀u1 u2 : set, u1 ∈ U → u2 ∈ U → apply_fun f u1 = apply_fun f u2 → u1 = u2.
Let u1 and u2 be given.
Assume Hu1U: u1 ∈ U.
Assume Hu2U: u2 ∈ U.
Assume Heq: apply_fun f u1 = apply_fun f u2.
An exact proof term for the current goal is (homeomorphism_injective U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f Hhomeo u1 u2 Hu1U Hu2U Heq).
We prove the intermediate claim Hneqf: apply_fun f y ≠ apply_fun f x0.
Assume Heqf: apply_fun f y = apply_fun f x0.
We prove the intermediate claim Hyx0: y = x0.
An exact proof term for the current goal is (Hinj y x0 HyU Hx0U Heqf).
An exact proof term for the current goal is (Hyneq Hyx0).
Set O to be the term V ∖ {apply_fun f x0}.
We prove the intermediate claim HOopen: O ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V.
An exact proof term for the current goal is (T1_singleton_complement_open V (subspace_topology (euclidean_space m) (euclidean_topology m) V) (apply_fun f x0) HT1V Hfx0V).
We prove the intermediate claim HfyO: apply_fun f y ∈ O.
Apply setminusI to the current goal.
An exact proof term for the current goal is HfyV.
Assume Hsing: apply_fun f y ∈ {apply_fun f x0}.
We prove the intermediate claim Heqf: apply_fun f y = apply_fun f x0.
An exact proof term for the current goal is (SingE (apply_fun f x0) (apply_fun f y) Hsing).
An exact proof term for the current goal is (Hneqf Heqf).
We prove the intermediate claim Hpreimg_open: preimage_of U f O ∈ subspace_topology X Tx U.
We prove the intermediate claim Hpreimg_axiom: ∀V1 : set, V1 ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V → preimage_of U f V1 ∈ subspace_topology X Tx U.
An exact proof term for the current goal is (andER ((topology_on U (subspace_topology X Tx U) ∧ topology_on V (subspace_topology (euclidean_space m) (euclidean_topology m) V)) ∧ function_on f U V) (∀V1 : set, V1 ∈ subspace_topology (euclidean_space m) (euclidean_topology m) V → preimage_of U f V1 ∈ subspace_topology X Tx U) Hcontf).
An exact proof term for the current goal is (Hpreimg_axiom O HOopen).
We prove the intermediate claim Hpreimg_sub: preimage_of U f O ⊆ U.
Let z be given.
Assume Hz: z ∈ preimage_of U f O.
An exact proof term for the current goal is (SepE1 U (λu : set ⇒ apply_fun f u ∈ O) z Hz).
We prove the intermediate claim Hpreimg_open_in: open_in U (subspace_topology X Tx U) (preimage_of U f O).
We will prove topology_on U (subspace_topology X Tx U) ∧ preimage_of U f O ∈ subspace_topology X Tx U.
Apply andI to the current goal.
An exact proof term for the current goal is HTU.
An exact proof term for the current goal is Hpreimg_open.
We prove the intermediate claim HexV0: ∃V0 ∈ Tx, preimage_of U f O = V0 ∩ U.
An exact proof term for the current goal is (iffEL (open_in U (subspace_topology X Tx U) (preimage_of U f O)) (∃V0 ∈ Tx, preimage_of U f O = V0 ∩ U) (open_in_subspace_iff X Tx U (preimage_of U f O) Htop HUsubX Hpreimg_sub) Hpreimg_open_in).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0conj: V0 ∈ Tx ∧ preimage_of U f O = V0 ∩ U.
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (preimage_of U f O = V0 ∩ U) HV0conj).
We prove the intermediate claim HeqW: preimage_of U f O = V0 ∩ U.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (preimage_of U f O = V0 ∩ U) HV0conj).
We use (V0 ∩ U) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_binintersect_closed X Tx V0 U Htop HV0Tx HUinTx).
rewrite the current goal using HeqW (from right to left).
We will prove y ∈ preimage_of U f O.
We will prove y ∈ {u ∈ U|apply_fun f u ∈ O}.
Apply (SepI U (λu : set ⇒ apply_fun f u ∈ O) y HyU) to the current goal.
An exact proof term for the current goal is HfyO.
Assume Hx0W: x0 ∈ (V0 ∩ U).
We prove the intermediate claim Hx0Pre: x0 ∈ preimage_of U f O.
rewrite the current goal using HeqW (from left to right).
An exact proof term for the current goal is Hx0W.
We prove the intermediate claim Hfx0O: apply_fun f x0 ∈ O.
An exact proof term for the current goal is (SepE2 U (λu : set ⇒ apply_fun f u ∈ O) x0 Hx0Pre).
We prove the intermediate claim HnotSing: apply_fun f x0 ∉ {apply_fun f x0}.
An exact proof term for the current goal is (setminusE2 V {apply_fun f x0} (apply_fun f x0) Hfx0O).
An exact proof term for the current goal is (HnotSing (SingI (apply_fun f x0))).
Assume Hx0notU: ¬ (x0 ∈ U).
We use U to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HUopen).
An exact proof term for the current goal is HyU.
An exact proof term for the current goal is Hx0notU.
We prove the intermediate claim Hcomp_open: X ∖ {x0} ∈ Tx.
Set UFam to be the term {W ∈ 𝒫 X|∃y : set, y ∈ X ∧ y ≠ x0 ∧ W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W}.
We prove the intermediate claim HUFamSub: UFam ⊆ Tx.
Let W be given.
Assume HW: W ∈ UFam.
We prove the intermediate claim HWpred: ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λW0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W0 ∈ Tx ∧ y ∈ W0 ∧ x0 ∉ W0) W HW).
Apply HWpred to the current goal.
Let y be given.
Assume Hy_conj: y ∈ X ∧ y ≠ x0 ∧ W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W.
We prove the intermediate claim H0: (((y ∈ X ∧ y ≠ x0) ∧ W ∈ Tx) ∧ y ∈ W).
An exact proof term for the current goal is (andEL ((((y ∈ X ∧ y ≠ x0) ∧ W ∈ Tx) ∧ y ∈ W)) (x0 ∉ W) Hy_conj).
We prove the intermediate claim H1: (y ∈ X ∧ y ≠ x0) ∧ W ∈ Tx.
An exact proof term for the current goal is (andEL ((y ∈ X ∧ y ≠ x0) ∧ W ∈ Tx) (y ∈ W) H0).
An exact proof term for the current goal is (andER (y ∈ X ∧ y ≠ x0) (W ∈ Tx) H1).
We prove the intermediate claim HUnionOpen: ⋃ UFam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx UFam Htop HUFamSub).
We prove the intermediate claim HUnionEq: ⋃ UFam = X ∖ {x0}.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ ⋃ UFam.
We will prove z ∈ X ∖ {x0}.
Apply (UnionE_impred UFam z Hz (z ∈ X ∖ {x0})) to the current goal.
Let W be given.
Assume HzW: z ∈ W.
Assume HW: W ∈ UFam.
We prove the intermediate claim HWpow: W ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λW0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W0 ∈ Tx ∧ y ∈ W0 ∧ x0 ∉ W0) W HW).
We prove the intermediate claim HWsubX: W ⊆ X.
An exact proof term for the current goal is (PowerE X W HWpow).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (HWsubX z HzW).
We prove the intermediate claim HWpred: ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λW0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W0 ∈ Tx ∧ y ∈ W0 ∧ x0 ∉ W0) W HW).
Apply HWpred to the current goal.
Let y be given.
Assume Hy_conj: y ∈ X ∧ y ≠ x0 ∧ W ∈ Tx ∧ y ∈ W ∧ x0 ∉ W.
We prove the intermediate claim Hx0NotW: x0 ∉ W.
An exact proof term for the current goal is (andER ((((y ∈ X ∧ y ≠ x0) ∧ W ∈ Tx) ∧ y ∈ W)) (x0 ∉ W) Hy_conj).
We prove the intermediate claim HznotSing: z ∉ {x0}.
Assume HzSing: z ∈ {x0}.
We prove the intermediate claim Hzeq: z = x0.
An exact proof term for the current goal is (SingE x0 z HzSing).
We prove the intermediate claim Hx0W: x0 ∈ W.
rewrite the current goal using Hzeq (from right to left).
An exact proof term for the current goal is HzW.
An exact proof term for the current goal is (Hx0NotW Hx0W).
An exact proof term for the current goal is (setminusI X {x0} z HzX HznotSing).
Let z be given.
Assume Hz: z ∈ X ∖ {x0}.
We will prove z ∈ ⋃ UFam.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (setminusE1 X {x0} z Hz).
We prove the intermediate claim HznotSing: z ∉ {x0}.
An exact proof term for the current goal is (setminusE2 X {x0} z Hz).
We prove the intermediate claim Hzneq: z ≠ x0.
Assume Hzeq: z = x0.
We prove the intermediate claim HzSing: z ∈ {x0}.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (SingI x0).
An exact proof term for the current goal is (HznotSing HzSing).
We prove the intermediate claim HexW: ∃W : set, W ∈ Tx ∧ z ∈ W ∧ x0 ∉ W.
An exact proof term for the current goal is (Hsep_x0 z HzX Hzneq).
Apply HexW to the current goal.
Let W be given.
Assume HWconj: W ∈ Tx ∧ z ∈ W ∧ x0 ∉ W.
We prove the intermediate claim HW0: W ∈ Tx ∧ z ∈ W.
An exact proof term for the current goal is (andEL (W ∈ Tx ∧ z ∈ W) (x0 ∉ W) HWconj).
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (andEL (W ∈ Tx) (z ∈ W) HW0).
We prove the intermediate claim HzW: z ∈ W.
An exact proof term for the current goal is (andER (W ∈ Tx) (z ∈ W) HW0).
We prove the intermediate claim Hx0notW: x0 ∉ W.
An exact proof term for the current goal is (andER (W ∈ Tx ∧ z ∈ W) (x0 ∉ W) HWconj).
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx Htop).
We prove the intermediate claim HWpow: W ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub W HWTx).
We prove the intermediate claim HWUFam: W ∈ UFam.
Apply (SepI (𝒫 X) (λW0 : set ⇒ ∃y : set, y ∈ X ∧ y ≠ x0 ∧ W0 ∈ Tx ∧ y ∈ W0 ∧ x0 ∉ W0) W HWpow) to the current goal.
We use z to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzX.
An exact proof term for the current goal is Hzneq.
An exact proof term for the current goal is HWTx.
An exact proof term for the current goal is HzW.
An exact proof term for the current goal is Hx0notW.
An exact proof term for the current goal is (UnionI UFam z W HzW HWUFam).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionOpen.
We will prove topology_on X Tx ∧ ({x0} ⊆ X ∧ ∃U ∈ Tx, {x0} = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Apply andI to the current goal.
An exact proof term for the current goal is HsingSub.
We use (X ∖ {x0}) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hcomp_open.
rewrite the current goal using (setminus_setminus_eq X {x0} HsingSub) (from left to right).
Use reflexivity.
∎