Let X, Tx and m be given.
Assume Hloc: locally_m_euclidean X Tx m.
Assume Hcomp: compact_space X Tx.
We will prove second_countable_space X Tx.
We prove the intermediate claim HmTx: m ∈ ω ∧ topology_on X Tx.
An exact proof term for the current goal is (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) Hloc).
We prove the intermediate claim Hm: m ∈ ω.
An exact proof term for the current goal is (andEL (m ∈ ω) (topology_on X Tx) 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) HmTx).
We prove the intermediate claim Hchart: ∀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) Hloc).
We prove the intermediate claim HL: Lindelof_space X Tx.
An exact proof term for the current goal is (compact_space_implies_Lindelof_space X Tx Hcomp).
We prove the intermediate claim HLprop: ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V) HL).
Set ChartDomains to be the term {U ∈ Tx|∃x : set, x ∈ X ∧ ∃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}.
We prove the intermediate claim HcovCharts: open_cover X Tx ChartDomains.
We will prove (∀u : set, u ∈ ChartDomains → u ∈ Tx) ∧ covers X ChartDomains.
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ ChartDomains.
We will prove u ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x : set, x ∈ X ∧ ∃V : set, ∃f : set, open_in X Tx U0 ∧ x ∈ U0 ∧ V ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V ∧ homeomorphism U0 (subspace_topology X Tx U0) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f) u Hu).
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃u : set, u ∈ ChartDomains ∧ x ∈ u.
Apply (Hchart 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 V0 be given.
Assume Hexf: ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f.
Apply Hexf to the current goal.
Let f be given.
Assume HUpack.
We prove the intermediate claim Hleft1: (((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0).
An exact proof term for the current goal is (andEL (((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0) (homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f) HUpack).
We prove the intermediate claim Hleft2: (open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ euclidean_space m.
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ euclidean_space m) (open_in (euclidean_space m) (euclidean_topology m) V0) Hleft1).
We prove the intermediate claim Hleft3: open_in X Tx U ∧ x ∈ U.
An exact proof term for the current goal is (andEL (open_in X Tx U ∧ x ∈ U) (V0 ⊆ euclidean_space m) Hleft2).
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) (x ∈ U) Hleft3).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HUopen).
We use U to witness the existential quantifier.
Apply andI to the current goal.
We will prove U ∈ ChartDomains.
Apply (SepI Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∧ ∃V1 : set, ∃f1 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V1 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V1 ∧ homeomorphism U0 (subspace_topology X Tx U0) V1 (subspace_topology (euclidean_space m) (euclidean_topology m) V1) f1) U) to the current goal.
An exact proof term for the current goal is HUinTx.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
We use V0 to witness the existential quantifier.
We use f to witness the existential quantifier.
An exact proof term for the current goal is HUpack.
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) Hleft3).
An exact proof term for the current goal is HxU.
Apply (HLprop ChartDomains HcovCharts) to the current goal.
Let V be given.
Assume HVpack: countable_subcollection V ChartDomains ∧ covers X V.
We prove the intermediate claim HVsub: V ⊆ ChartDomains.
An exact proof term for the current goal is (andEL (V ⊆ ChartDomains) (countable_set V) (andEL (countable_subcollection V ChartDomains) (covers X V) HVpack)).
We prove the intermediate claim HVcount: countable_set V.
An exact proof term for the current goal is (andER (V ⊆ ChartDomains) (countable_set V) (andEL (countable_subcollection V ChartDomains) (covers X V) HVpack)).
We prove the intermediate claim HcovV: covers X V.
An exact proof term for the current goal is (andER (countable_subcollection V ChartDomains) (covers X V) HVpack).
Set Bsel to be the term λU : set ⇒ Eps_i (λB : set ⇒ basis_on U B ∧ countable_set B ∧ basis_generates U B (subspace_topology X Tx U)) of type set → set.
We prove the intermediate claim HBsel_spec: ∀U : set, U ∈ V → basis_on U (Bsel U) ∧ countable_set (Bsel U) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
Let U be given.
Assume HUv: U ∈ V.
We will prove basis_on U (Bsel U) ∧ countable_set (Bsel U) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
We prove the intermediate claim HUchart: U ∈ ChartDomains.
An exact proof term for the current goal is (HVsub U HUv).
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x : set, x ∈ X ∧ ∃V0 : set, ∃f : set, open_in X Tx U0 ∧ x ∈ 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) f) U HUchart).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HUdata: ∃x : set, x ∈ X ∧ ∃V0 : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃x0 : set, x0 ∈ X ∧ ∃V1 : set, ∃f1 : set, open_in X Tx U0 ∧ x0 ∈ U0 ∧ V1 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V1 ∧ homeomorphism U0 (subspace_topology X Tx U0) V1 (subspace_topology (euclidean_space m) (euclidean_topology m) V1) f1) U HUchart).
Apply HUdata to the current goal.
Let x be given.
Assume Hxpack.
Apply Hxpack to the current goal.
Assume HxX: x ∈ X.
Assume HexV0: ∃V0 : set, ∃f : set, open_in X Tx U ∧ x ∈ U ∧ V0 ⊆ (euclidean_space m) ∧ open_in (euclidean_space m) (euclidean_topology m) V0 ∧ homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f.
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pack.
Apply HV0pack to the current goal.
Let f be given.
Assume Hpack.
We prove the intermediate claim Hpack1: (((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V0).
An exact proof term for the current goal is (andEL (((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V0) (homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f) Hpack).
We prove the intermediate claim Hpack2: (open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ (euclidean_space m).
An exact proof term for the current goal is (andEL ((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ (euclidean_space m)) (open_in (euclidean_space m) (euclidean_topology m) V0) Hpack1).
We prove the intermediate claim HV0sub: V0 ⊆ (euclidean_space m).
An exact proof term for the current goal is (andER (open_in X Tx U ∧ x ∈ U) (V0 ⊆ (euclidean_space m)) Hpack2).
We prove the intermediate claim Hhom: homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f.
An exact proof term for the current goal is (andER (((open_in X Tx U ∧ x ∈ U) ∧ V0 ⊆ (euclidean_space m)) ∧ open_in (euclidean_space m) (euclidean_topology m) V0) (homeomorphism U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f) Hpack).
We prove the intermediate claim HscE: second_countable_space (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (euclidean_spaces_second_countable m Hm).
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)) (∃B : set, basis_on (euclidean_space m) B ∧ countable_set B ∧ basis_generates (euclidean_space m) B (euclidean_topology m)) HscE).
We prove the intermediate claim HcountAx: (∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → second_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → second_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)).
An exact proof term for the current goal is (countability_axioms_subspace_product (euclidean_space m) (euclidean_topology m) HtopE).
We prove the intermediate claim Hleft: ((∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A))) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)).
An exact proof term for the current goal is (andEL (((∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A))) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi))) (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → second_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → second_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)) HcountAx).
We prove the intermediate claim H12: (∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)).
An exact proof term for the current goal is (andEL ((∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) ∧ (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A))) (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)) Hleft).
We prove the intermediate claim HscSub: ∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A).
An exact proof term for the current goal is (andER (∀A : set, A ⊆ (euclidean_space m) → first_countable_space (euclidean_space m) (euclidean_topology m) → first_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) (∀A : set, A ⊆ (euclidean_space m) → second_countable_space (euclidean_space m) (euclidean_topology m) → second_countable_space A (subspace_topology (euclidean_space m) (euclidean_topology m) A)) H12).
We prove the intermediate claim HscV0: second_countable_space V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0).
An exact proof term for the current goal is (HscSub V0 HV0sub HscE).
We prove the intermediate claim HscU: second_countable_space U (subspace_topology X Tx U).
An exact proof term for the current goal is (homeomorphism_preserves_second_countable U (subspace_topology X Tx U) V0 (subspace_topology (euclidean_space m) (euclidean_topology m) V0) f Hhom HscV0).
We prove the intermediate claim HexB: ∃B : set, basis_on U B ∧ countable_set B ∧ basis_generates U B (subspace_topology X Tx U).
An exact proof term for the current goal is (andER (topology_on U (subspace_topology X Tx U)) (∃B : set, basis_on U B ∧ countable_set B ∧ basis_generates U B (subspace_topology X Tx U)) HscU).
Set Bu to be the term Eps_i (λB : set ⇒ basis_on U B ∧ countable_set B ∧ basis_generates U B (subspace_topology X Tx U)).
We prove the intermediate claim HBu: basis_on U Bu ∧ countable_set Bu ∧ basis_generates U Bu (subspace_topology X Tx U).
An exact proof term for the current goal is (Eps_i_ex (λB : set ⇒ basis_on U B ∧ countable_set B ∧ basis_generates U B (subspace_topology X Tx U)) HexB).
We prove the intermediate claim HBselEq: Bsel U = Bu.
Use reflexivity.
rewrite the current goal using HBselEq (from left to right).
An exact proof term for the current goal is HBu.
Set Pair to be the term ∑U ∈ V, Bsel U.
Set Fp to be the term λp : set ⇒ p 1 of type set → set.
Set B to be the term {Fp p|p ∈ Pair}.
We prove the intermediate claim HPairCount: countable_set Pair.
We prove the intermediate claim HVc: countable V.
An exact proof term for the current goal is HVcount.
We prove the intermediate claim HBfib: ∀U : set, U ∈ V → countable (Bsel U).
Let U be given.
Assume HUv: U ∈ V.
We prove the intermediate claim Hspec: basis_on U (Bsel U) ∧ countable_set (Bsel U) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is (HBsel_spec U HUv).
We prove the intermediate claim Hmid: (basis_on U (Bsel U) ∧ countable_set (Bsel U)) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is Hspec.
We prove the intermediate claim Hpair: basis_on U (Bsel U) ∧ countable_set (Bsel U).
An exact proof term for the current goal is (andEL (basis_on U (Bsel U) ∧ countable_set (Bsel U)) (basis_generates U (Bsel U) (subspace_topology X Tx U)) Hmid).
We prove the intermediate claim Hcount: countable_set (Bsel U).
An exact proof term for the current goal is (andER (basis_on U (Bsel U)) (countable_set (Bsel U)) Hpair).
An exact proof term for the current goal is Hcount.
We prove the intermediate claim HPairC: countable Pair.
An exact proof term for the current goal is (Sigma_countable V HVc Bsel HBfib).
An exact proof term for the current goal is HPairC.
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (countable_image Pair HPairCount Fp).
We prove the intermediate claim HBsubTx: ∀b : set, b ∈ B → b ∈ Tx.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ Tx.
Apply (ReplE_impred Pair Fp b HbB) to the current goal.
Let p be given.
Assume HpPair: p ∈ Pair.
Assume HbEq: b = Fp p.
Apply (Sigma_E V Bsel p HpPair) to the current goal.
Let U be given.
Assume HUpair.
Apply HUpair to the current goal.
Assume HUv: U ∈ V.
Assume Hexy.
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
Apply Hypair to the current goal.
Assume Hy: y ∈ Bsel U.
Assume HpEq.
We prove the intermediate claim Hp1: (p 1) = y.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (pair_ap_1 U y).
We prove the intermediate claim HBspec: basis_on U (Bsel U) ∧ countable_set (Bsel U) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is (HBsel_spec U HUv).
We prove the intermediate claim HBmid: (basis_on U (Bsel U) ∧ countable_set (Bsel U)) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is HBspec.
We prove the intermediate claim HBpair: basis_on U (Bsel U) ∧ countable_set (Bsel U).
An exact proof term for the current goal is (andEL (basis_on U (Bsel U) ∧ countable_set (Bsel U)) (basis_generates U (Bsel U) (subspace_topology X Tx U)) HBmid).
We prove the intermediate claim HBasisU: basis_on U (Bsel U).
An exact proof term for the current goal is (andEL (basis_on U (Bsel U)) (countable_set (Bsel U)) HBpair).
We prove the intermediate claim HBUgen: basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is (andER (basis_on U (Bsel U) ∧ countable_set (Bsel U)) (basis_generates U (Bsel U) (subspace_topology X Tx U)) HBmid).
We prove the intermediate claim HgenEq: generated_topology U (Bsel U) = subspace_topology X Tx U.
An exact proof term for the current goal is (andER (basis_on U (Bsel U)) (generated_topology U (Bsel U) = subspace_topology X Tx U) HBUgen).
We prove the intermediate claim HyGen: y ∈ generated_topology U (Bsel U).
An exact proof term for the current goal is (generated_topology_contains_basis U (Bsel U) HBasisU y Hy).
We prove the intermediate claim HySubspace: y ∈ subspace_topology X Tx U.
We will prove y ∈ subspace_topology X Tx U.
rewrite the current goal using HgenEq (from right to left).
An exact proof term for the current goal is HyGen.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃x : set, x ∈ X ∧ ∃V0 : set, ∃f : set, open_in X Tx U0 ∧ x ∈ 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) f) U (HVsub U HUv)).
We prove the intermediate claim HysubU: y ⊆ U.
We prove the intermediate claim HBpow: (Bsel U) ⊆ 𝒫 U.
An exact proof term for the current goal is (basis_on_sub_Power U (Bsel U) HBasisU).
We prove the intermediate claim HyPow: y ∈ 𝒫 U.
An exact proof term for the current goal is (HBpow y Hy).
An exact proof term for the current goal is (PowerE U y HyPow).
We prove the intermediate claim HyOpen: open_in U (subspace_topology X Tx U) y.
We will prove topology_on U (subspace_topology X Tx U) ∧ y ∈ subspace_topology X Tx U.
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx U HTx (topology_elem_subset X Tx U HTx HUinTx)).
An exact proof term for the current goal is HySubspace.
We prove the intermediate claim HyTx: y ∈ Tx.
An exact proof term for the current goal is (open_in_subspace_if_ambient_open X Tx U y HTx HUinTx HysubU HyOpen).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim HFpEq: Fp p = (p 1).
Use reflexivity.
rewrite the current goal using HFpEq (from left to right).
rewrite the current goal using Hp1 (from left to right).
An exact proof term for the current goal is HyTx.
We prove the intermediate claim HBrefines: ∀U0 ∈ Tx, ∀x ∈ U0, ∃Cx ∈ B, x ∈ Cx ∧ Cx ⊆ U0.
Let U0 be given.
Assume HU0: U0 ∈ Tx.
Let x be given.
Assume HxU0: x ∈ U0.
We will prove ∃Cx ∈ B, x ∈ Cx ∧ Cx ⊆ U0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0 x HxU0).
We prove the intermediate claim HexU: ∃U : set, U ∈ V ∧ x ∈ U.
An exact proof term for the current goal is (HcovV x HxX).
Apply HexU to the current goal.
Let U be given.
Assume HUvx: U ∈ V ∧ x ∈ U.
We prove the intermediate claim HUv: U ∈ V.
An exact proof term for the current goal is (andEL (U ∈ V) (x ∈ U) HUvx).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ V) (x ∈ U) HUvx).
Set A to be the term U0 ∩ U.
We prove the intermediate claim HAinSub: A ∈ subspace_topology X Tx U.
We prove the intermediate claim HAeq: A = U0 ∩ U.
Use reflexivity.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx U U0 HU0).
We prove the intermediate claim HBspec: basis_on U (Bsel U) ∧ countable_set (Bsel U) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is (HBsel_spec U HUv).
We prove the intermediate claim HBmid: (basis_on U (Bsel U) ∧ countable_set (Bsel U)) ∧ basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is HBspec.
We prove the intermediate claim HBUgen: basis_generates U (Bsel U) (subspace_topology X Tx U).
An exact proof term for the current goal is (andER (basis_on U (Bsel U) ∧ countable_set (Bsel U)) (basis_generates U (Bsel U) (subspace_topology X Tx U)) HBmid).
We prove the intermediate claim HgenEq: generated_topology U (Bsel U) = subspace_topology X Tx U.
An exact proof term for the current goal is (andER (basis_on U (Bsel U)) (generated_topology U (Bsel U) = subspace_topology X Tx U) HBUgen).
We prove the intermediate claim HAgen: A ∈ generated_topology U (Bsel U).
We will prove A ∈ generated_topology U (Bsel U).
rewrite the current goal using HgenEq (from left to right).
An exact proof term for the current goal is HAinSub.
We prove the intermediate claim HrefA: ∀z ∈ A, ∃b ∈ (Bsel U), z ∈ b ∧ b ⊆ A.
An exact proof term for the current goal is (SepE2 (𝒫 U) (λU1 : set ⇒ ∀z0 ∈ U1, ∃b0 ∈ (Bsel U), z0 ∈ b0 ∧ b0 ⊆ U1) A HAgen).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectI U0 U x HxU0 HxU).
We prove the intermediate claim Hexb: ∃b ∈ (Bsel U), x ∈ b ∧ b ⊆ A.
An exact proof term for the current goal is (HrefA x HxA).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpack.
We prove the intermediate claim HbIn: b ∈ (Bsel U).
An exact proof term for the current goal is (andEL (b ∈ (Bsel U)) (x ∈ b ∧ b ⊆ A) Hbpack).
We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ A.
An exact proof term for the current goal is (andER (b ∈ (Bsel U)) (x ∈ b ∧ b ⊆ A) Hbpack).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ A) Hbprop).
We prove the intermediate claim HbsubA: b ⊆ A.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ A) Hbprop).
We prove the intermediate claim HbsubU0: b ⊆ U0.
Let z be given.
Assume Hz: z ∈ b.
We prove the intermediate claim HzA: z ∈ A.
An exact proof term for the current goal is (HbsubA z Hz).
An exact proof term for the current goal is (binintersectE1 U0 U z HzA).
We prove the intermediate claim HpSig: (U,b) ∈ Pair.
An exact proof term for the current goal is (tuple_2_Sigma V Bsel U HUv b HbIn).
We prove the intermediate claim HFp: Fp (U,b) = b.
We prove the intermediate claim HFdef: Fp (U,b) = ((U,b) 1).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (tuple_2_1_eq U b) (from left to right).
Use reflexivity.
Set Cx to be the term b.
We use Cx to witness the existential quantifier.
Apply andI to the current goal.
We will prove Cx ∈ B.
rewrite the current goal using HFp (from right to left).
An exact proof term for the current goal is (ReplI Pair Fp (U,b) HpSig).
Apply andI to the current goal.
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is HbsubU0.
We prove the intermediate claim HBasisEq: basis_on X B ∧ generated_topology X B = Tx.
An exact proof term for the current goal is (basis_refines_topology X Tx B HTx HBsubTx HBrefines).
We prove the intermediate claim HBgener: basis_generates X B Tx.
We will prove basis_on X B ∧ generated_topology X B = Tx.
An exact proof term for the current goal is HBasisEq.
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (generated_topology X B = Tx) HBasisEq).
We will prove topology_on X Tx ∧ ∃B0 : set, basis_on X B0 ∧ countable_set B0 ∧ basis_generates X B0 Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We use B to witness the existential quantifier.
We will prove basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
Apply andI to the current goal.
An exact proof term for the current goal is (andI (basis_on X B) (countable_set B) HBasis HBcount).
An exact proof term for the current goal is HBgener.
∎