We will prove dense_in (U_eps X Tx Y d fn eps) X Tx.

We will prove closure_of X Tx (U_eps X Tx Y d fn eps) = X.

Apply set_ext to the current goal.

An exact proof term for the current goal is (closure_in_space X Tx (U_eps X Tx Y d fn eps) HTx).

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ closure_of X Tx (U_eps X Tx Y d fn eps).

We prove the intermediate claim Hcliff: x ∈ closure_of X Tx (U_eps X Tx Y d fn eps) ↔ (∀U ∈ Tx, x ∈ U → U ∩ (U_eps X Tx Y d fn eps) ≠ Empty).

An exact proof term for the current goal is (closure_characterization X Tx (U_eps X Tx Y d fn eps) x HTx HxX).

Apply (iffER (x ∈ closure_of X Tx (U_eps X Tx Y d fn eps)) (∀U ∈ Tx, x ∈ U → U ∩ (U_eps X Tx Y d fn eps) ≠ Empty) Hcliff) to the current goal.

We will prove ∀U ∈ Tx, x ∈ U → U ∩ (U_eps X Tx Y d fn eps) ≠ Empty.

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We prove the intermediate claim HUne: U ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty U x HxU).

We prove the intermediate claim HUopen: open_in X Tx U.

An exact proof term for the current goal is (open_inI X Tx U HTx HU).

We prove the intermediate claim HBU: Baire_space U (subspace_topology X Tx U).

An exact proof term for the current goal is (Baire_open_subspace X Tx U HB HUopen).

We prove the intermediate claim HBcU: Baire_space_closed U (subspace_topology X Tx U).

An exact proof term for the current goal is (Baire_space_imp_closed U (subspace_topology X Tx U) HBU).

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 HTx (open_in_subset X Tx U HUopen)).

We prove the intermediate claim HBUprop: ∀Fam : set, countable_set Fam → (∀A : set, A ∈ Fam → closed_in U (subspace_topology X Tx U) A ∧ interior_of U (subspace_topology X Tx U) A = Empty) → interior_of U (subspace_topology X Tx U) (⋃ Fam) = Empty.

An exact proof term for the current goal is (andER (topology_on U (subspace_topology X Tx U)) (∀Fam : set, countable_set Fam → (∀A : set, A ∈ Fam → closed_in U (subspace_topology X Tx U) A ∧ interior_of U (subspace_topology X Tx U) A = Empty) → interior_of U (subspace_topology X Tx U) (⋃ Fam) = Empty) HBcU).

Set Fam to be the term {U ∩ (A_N_eps X Y d fn N eps)|N ∈ ω}.

We prove the intermediate claim HomegaCount: countable_set ω.

We will prove countable_set ω.

We will prove countable ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

We prove the intermediate claim HcountFam: countable_set Fam.

An exact proof term for the current goal is (countable_image ω HomegaCount (λN0 : set ⇒ U ∩ (A_N_eps X Y d fn N0 eps))).

We prove the intermediate claim HFamClosed: ∀B : set, B ∈ Fam → closed_in U (subspace_topology X Tx U) B.

Let B be given.

Assume HBmem: B ∈ Fam.

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ B = U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (ReplE ω (λN0 : set ⇒ U ∩ (A_N_eps X Y d fn N0 eps)) B HBmem).

Apply HexN to the current goal.

Let N be given.

Assume HN: N ∈ ω ∧ B = U ∩ (A_N_eps X Y d fn N eps).

We prove the intermediate claim HNin: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (B = U ∩ (A_N_eps X Y d fn N eps)) HN).

We prove the intermediate claim HBdef: B = U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (andER (N ∈ ω) (B = U ∩ (A_N_eps X Y d fn N eps)) HN).

We prove the intermediate claim HclX: closed_in X Tx (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (Hclosed N HNin).

We prove the intermediate claim HsubU: U ⊆ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU).

We prove the intermediate claim HBclosedU: closed_in U (subspace_topology X Tx U) (A_N_eps X Y d fn N eps ∩ U).

Apply (iffER (closed_in U (subspace_topology X Tx U) (A_N_eps X Y d fn N eps ∩ U)) (∃C : set, closed_in X Tx C ∧ (A_N_eps X Y d fn N eps ∩ U) = C ∩ U) (closed_in_subspace_iff_intersection X Tx U (A_N_eps X Y d fn N eps ∩ U) HTx HsubU)) to the current goal.

We use (A_N_eps X Y d fn N eps) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HclX.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ (A_N_eps X Y d fn N eps ∩ U).

An exact proof term for the current goal is Hz.

Let z be given.

Assume Hz: z ∈ (A_N_eps X Y d fn N eps ∩ U).

An exact proof term for the current goal is Hz.

rewrite the current goal using HBdef (from left to right).

We prove the intermediate claim Hcomm: U ∩ (A_N_eps X Y d fn N eps) = (A_N_eps X Y d fn N eps) ∩ U.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ U ∩ (A_N_eps X Y d fn N eps).

We will prove z ∈ (A_N_eps X Y d fn N eps) ∩ U.

An exact proof term for the current goal is (binintersectI (A_N_eps X Y d fn N eps) U z (binintersectE2 U (A_N_eps X Y d fn N eps) z Hz) (binintersectE1 U (A_N_eps X Y d fn N eps) z Hz)).

Let z be given.

Assume Hz: z ∈ (A_N_eps X Y d fn N eps) ∩ U.

We will prove z ∈ U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (binintersectI U (A_N_eps X Y d fn N eps) z (binintersectE2 (A_N_eps X Y d fn N eps) U z Hz) (binintersectE1 (A_N_eps X Y d fn N eps) U z Hz)).

rewrite the current goal using Hcomm (from left to right).

An exact proof term for the current goal is HBclosedU.

We prove the intermediate claim HexNgood: ∃N : set, N ∈ ω ∧ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty.

Apply (xm (∃N : set, N ∈ ω ∧ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty)) to the current goal.

Assume Hex.

An exact proof term for the current goal is Hex.

Assume Hno: ¬ (∃N : set, N ∈ ω ∧ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty).

We will prove ∃N : set, N ∈ ω ∧ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty.

Apply FalseE to the current goal.

We prove the intermediate claim HFamPack: ∀B : set, B ∈ Fam → closed_in U (subspace_topology X Tx U) B ∧ interior_of U (subspace_topology X Tx U) B = Empty.

Let B be given.

Assume HBmem: B ∈ Fam.

We prove the intermediate claim HBcl: closed_in U (subspace_topology X Tx U) B.

An exact proof term for the current goal is (HFamClosed B HBmem).

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ B = U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (ReplE ω (λN0 : set ⇒ U ∩ (A_N_eps X Y d fn N0 eps)) B HBmem).

Apply HexN to the current goal.

Let N be given.

Assume HN: N ∈ ω ∧ B = U ∩ (A_N_eps X Y d fn N eps).

We prove the intermediate claim HNin: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (B = U ∩ (A_N_eps X Y d fn N eps)) HN).

We prove the intermediate claim HBdef: B = U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (andER (N ∈ ω) (B = U ∩ (A_N_eps X Y d fn N eps)) HN).

We prove the intermediate claim Hempt: interior_of U (subspace_topology X Tx U) B = Empty.

rewrite the current goal using HBdef (from left to right).

Apply (xm (interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) = Empty)) to the current goal.

Assume Heq.

An exact proof term for the current goal is Heq.

Assume Hneq: interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty.

Apply FalseE to the current goal.

Apply Hno to the current goal.

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HNin.

An exact proof term for the current goal is Hneq.

Apply andI to the current goal.

An exact proof term for the current goal is HBcl.

An exact proof term for the current goal is Hempt.

We prove the intermediate claim HintUnion: interior_of U (subspace_topology X Tx U) (⋃ Fam) = Empty.

An exact proof term for the current goal is (HBUprop Fam HcountFam HFamPack).

We prove the intermediate claim HUnionEq: ⋃ Fam = U.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ ⋃ Fam.

Apply (UnionE_impred Fam z Hz (z ∈ U)) to the current goal.

Let B be given.

Assume HzB: z ∈ B.

Assume HBmem: B ∈ Fam.

We prove the intermediate claim HBsubU: B ⊆ U.

Apply (ReplE_impred ω (λN0 : set ⇒ U ∩ (A_N_eps X Y d fn N0 eps)) B HBmem (B ⊆ U)) to the current goal.

Let N0 be given.

Assume _.

Assume HBdef.

rewrite the current goal using HBdef (from left to right).

An exact proof term for the current goal is (binintersect_Subq_1 U (A_N_eps X Y d fn N0 eps)).

An exact proof term for the current goal is (HBsubU z HzB).

Let z be given.

Assume HzU: z ∈ U.

We will prove z ∈ ⋃ Fam.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU z HzU).

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ z ∈ A_N_eps X Y d fn N eps.

An exact proof term for the current goal is (Hcover z HzX).

Apply HexN to the current goal.

Let N be given.

Assume HN: N ∈ ω ∧ z ∈ A_N_eps X Y d fn N eps.

We prove the intermediate claim HNin: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (z ∈ A_N_eps X Y d fn N eps) HN).

We prove the intermediate claim HzAN: z ∈ A_N_eps X Y d fn N eps.

An exact proof term for the current goal is (andER (N ∈ ω) (z ∈ A_N_eps X Y d fn N eps) HN).

We prove the intermediate claim HzB: z ∈ U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (binintersectI U (A_N_eps X Y d fn N eps) z HzU HzAN).

We prove the intermediate claim HBmem: (U ∩ (A_N_eps X Y d fn N eps)) ∈ Fam.

An exact proof term for the current goal is (ReplI ω (λN0 : set ⇒ U ∩ (A_N_eps X Y d fn N0 eps)) N HNin).

An exact proof term for the current goal is (UnionI Fam z (U ∩ (A_N_eps X Y d fn N eps)) HzB HBmem).

We prove the intermediate claim HintU: interior_of U (subspace_topology X Tx U) U = U.

An exact proof term for the current goal is (interior_of_space U (subspace_topology X Tx U) HTu).

We prove the intermediate claim HintUEmpty: interior_of U (subspace_topology X Tx U) U = Empty.

rewrite the current goal using HintUnion (from right to left).

rewrite the current goal using HUnionEq (from left to right).

Use reflexivity.

We prove the intermediate claim HUeqEmpty: U = Empty.

rewrite the current goal using HintU (from right to left).

An exact proof term for the current goal is HintUEmpty.

An exact proof term for the current goal is (HUne HUeqEmpty).

Apply HexNgood to the current goal.

Let N be given.

Assume HN: N ∈ ω ∧ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty.

We prove the intermediate claim HNin: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty) HN).

We prove the intermediate claim HintNe: interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty.

An exact proof term for the current goal is (andER (N ∈ ω) (interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)) ≠ Empty) HN).

We prove the intermediate claim Hexy: ∃y : set, y ∈ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)).

An exact proof term for the current goal is (nonempty_has_element (interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps))) HintNe).

Apply Hexy to the current goal.

Let y be given.

Assume HyInt: y ∈ interior_of U (subspace_topology X Tx U) (U ∩ (A_N_eps X Y d fn N eps)).

We prove the intermediate claim HyU: y ∈ U.

An exact proof term for the current goal is (SepE1 U (λy0 : set ⇒ ∃W : set, W ∈ subspace_topology X Tx U ∧ y0 ∈ W ∧ W ⊆ (U ∩ (A_N_eps X Y d fn N eps))) y HyInt).

We prove the intermediate claim HexW: ∃W : set, W ∈ subspace_topology X Tx U ∧ y ∈ W ∧ W ⊆ (U ∩ (A_N_eps X Y d fn N eps)).

An exact proof term for the current goal is (SepE2 U (λy0 : set ⇒ ∃W : set, W ∈ subspace_topology X Tx U ∧ y0 ∈ W ∧ W ⊆ (U ∩ (A_N_eps X Y d fn N eps))) y HyInt).

Apply HexW to the current goal.

Let W be given.

Assume HW: W ∈ subspace_topology X Tx U ∧ y ∈ W ∧ W ⊆ (U ∩ (A_N_eps X Y d fn N eps)).

We prove the intermediate claim HWpack: (W ∈ subspace_topology X Tx U ∧ y ∈ W) ∧ W ⊆ (U ∩ (A_N_eps X Y d fn N eps)).

An exact proof term for the current goal is HW.

We prove the intermediate claim HW1: W ∈ subspace_topology X Tx U ∧ y ∈ W.

An exact proof term for the current goal is (andEL (W ∈ subspace_topology X Tx U ∧ y ∈ W) (W ⊆ (U ∩ (A_N_eps X Y d fn N eps))) HWpack).

We prove the intermediate claim HWsub: W ⊆ (U ∩ (A_N_eps X Y d fn N eps)).

An exact proof term for the current goal is (andER (W ∈ subspace_topology X Tx U ∧ y ∈ W) (W ⊆ (U ∩ (A_N_eps X Y d fn N eps))) HWpack).

We prove the intermediate claim HyW: y ∈ W.

An exact proof term for the current goal is (andER (W ∈ subspace_topology X Tx U) (y ∈ W) HW1).

We prove the intermediate claim HWTy: W ∈ subspace_topology X Tx U.

An exact proof term for the current goal is (andEL (W ∈ subspace_topology X Tx U) (y ∈ W) HW1).

We prove the intermediate claim HexV: ∃V ∈ Tx, W = V ∩ U.

An exact proof term for the current goal is (subspace_topologyE X Tx U W HWTy).

Apply HexV to the current goal.

Let V be given.

Assume HV: V ∈ Tx ∧ W = V ∩ U.

We prove the intermediate claim HVin: V ∈ Tx.

An exact proof term for the current goal is (andEL (V ∈ Tx) (W = V ∩ U) HV).

We prove the intermediate claim HWdef: W = V ∩ U.

An exact proof term for the current goal is (andER (V ∈ Tx) (W = V ∩ U) HV).

We prove the intermediate claim HWTx: W ∈ Tx.

rewrite the current goal using HWdef (from left to right).

An exact proof term for the current goal is (lemma_intersection_two_open X Tx V U HTx HVin HU).

We prove the intermediate claim HWsubA: W ⊆ (A_N_eps X Y d fn N eps).

Let z be given.

Assume HzW: z ∈ W.

We prove the intermediate claim HzUA: z ∈ U ∩ (A_N_eps X Y d fn N eps).

An exact proof term for the current goal is (HWsub z HzW).

An exact proof term for the current goal is (binintersectE2 U (A_N_eps X Y d fn N eps) z HzUA).

We prove the intermediate claim HyIntX: y ∈ interior_of X Tx (A_N_eps X Y d fn N eps).

We prove the intermediate claim HyX: y ∈ X.

An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HU y HyU).

We prove the intermediate claim HdefInt: interior_of X Tx (A_N_eps X Y d fn N eps) = {x0 ∈ X|∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps)}.

Use reflexivity.

rewrite the current goal using HdefInt (from left to right).

Apply (SepI X (λx0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps)) y HyX) to the current goal.

We use W to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is HWTx.

An exact proof term for the current goal is HyW.

An exact proof term for the current goal is HWsubA.

We prove the intermediate claim HyInFam: interior_of X Tx (A_N_eps X Y d fn N eps) ∈ {interior_of X Tx (A_N_eps X Y d fn N0 eps)|N0 ∈ ω}.

An exact proof term for the current goal is (ReplI ω (λN0 : set ⇒ interior_of X Tx (A_N_eps X Y d fn N0 eps)) N HNin).

We prove the intermediate claim HyUeps: y ∈ U_eps X Tx Y d fn eps.

An exact proof term for the current goal is (UnionI {interior_of X Tx (A_N_eps X Y d fn N0 eps)|N0 ∈ ω} y (interior_of X Tx (A_N_eps X Y d fn N eps)) HyIntX HyInFam).

We prove the intermediate claim HyInter: y ∈ U ∩ (U_eps X Tx Y d fn eps).

An exact proof term for the current goal is (binintersectI U (U_eps X Tx Y d fn eps) y HyU HyUeps).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ (U_eps X Tx Y d fn eps)) y HyInter).