Let X, Tx and m be given.
Assume Hloc: locally_m_euclidean X Tx m.
Assume Hcomp: compact_space X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove m_manifold X Tx m.
We prove the intermediate claim HmTx: (m ∈ ω ∧ topology_on X Tx) ∧ ∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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.
An exact proof term for the current goal is Hloc.
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (andEL (m ∈ ω) (topology_on X Tx) (andEL (m ∈ ω ∧ topology_on X Tx) (∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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) HmTx)).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andER (m ∈ ω) (topology_on X Tx) (andEL (m ∈ ω ∧ topology_on X Tx) (∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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) HmTx)).
We prove the intermediate claim Hcharts: ∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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.
An exact proof term for the current goal is (andER (m ∈ ω ∧ topology_on X Tx) (∀x : set, x ∈ X → ∃U : set, ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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) HmTx).
We prove the intermediate claim Hscc: second_countable_space X Tx.
An exact proof term for the current goal is (compact_locally_m_euclidean_second_countable_early X Tx m Hloc Hcomp).
We will prove (((Hausdorff_space X Tx ∧ second_countable_space X Tx) ∧ m ∈ ω) ∧ ∀x : set, x ∈ X → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∃V : set, V ∈ (euclidean_topology m) ∧ ∃f : set, homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f).
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 HH.
An exact proof term for the current goal is Hscc.
An exact proof term for the current goal is HmO.
Let x be given.
Assume HxX: x ∈ X.
Apply (Hcharts x HxX) to the current goal.
Let U be given.
Assume HexV: ∃V : set, ∃f : set, open_in X Tx U ∧ x ∈ 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.
Apply HexV to the current goal.
Let V be given.
Assume Hexf: ∃f : set, open_in X Tx U ∧ x ∈ 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.
Apply Hexf to the current goal.
Let f be given.
Assume Hpack: open_in X Tx U ∧ x ∈ 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.
We prove the intermediate claim Hleft4: (((open_in X Tx U ∧ x ∈ 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 ∧ x ∈ 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) Hpack).
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 ∧ x ∈ 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) Hpack).
We prove the intermediate claim Habc: (open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m).
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft4).
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 ∧ x ∈ U) ∧ V ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V) Hleft4).
We prove the intermediate claim HopenU: open_in X Tx U.
An exact proof term for the current goal is (andEL (open_in X Tx U) (x ∈ U) (andEL (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) Habc)).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HopenU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (open_in X Tx U) (x ∈ U) (andEL (open_in X Tx U ∧ x ∈ U) (V ⊆ (euclidean_space m)) Habc)).
We prove the intermediate claim HVinTe: V ∈ euclidean_topology m.
An exact proof term for the current goal is (open_in_elem (euclidean_space m) (euclidean_topology m) V HVopen).
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 HUinTx.
An exact proof term for the current goal is HxU.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVinTe.
We use f to witness the existential quantifier.
An exact proof term for the current goal is Hhomeo.
∎