Let X, Tx, A and x be given.
Assume HT1: T1_space X Tx.
Assume HxX: x ∈ X.
We will prove limit_point_of X Tx A x ↔ (∀U ∈ Tx, x ∈ U → infinite (U ∩ A)).
We prove the intermediate claim Htop: topology_on X Tx.
An exact proof term for the current goal is (T1_space_topology X Tx HT1).
We prove the intermediate claim Hfinite_closed: ∀F : set, F ⊆ X → finite F → closed_in X Tx F.
Let F be given.
Assume HFsub.
Assume HFfin.
An exact proof term for the current goal is (T1_space_finite_closed X Tx F HT1 HFsub HFfin).
Apply iffI to the current goal.
Assume Hlim: limit_point_of X Tx A x.
We will prove ∀U ∈ Tx, x ∈ U → infinite (U ∩ A).
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove infinite (U ∩ A).
We will prove ¬ finite (U ∩ A).
Assume Hfin: finite (U ∩ A).
We prove the intermediate claim Hnbr: ∀W : set, W ∈ Tx → x ∈ W → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ x ∈ X) (∀W : set, W ∈ Tx → x ∈ W → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ W) Hlim).
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
Set F to be the term (U ∩ A) ∖ {x}.
We prove the intermediate claim HFsub: F ⊆ U ∩ A.
An exact proof term for the current goal is (setminus_Subq (U ∩ A) {x}).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (Subq_finite (U ∩ A) Hfin F HFsub).
We prove the intermediate claim HFsubX: F ⊆ X.
Let z be given.
Assume HzF: z ∈ F.
We prove the intermediate claim HzUA: z ∈ U ∩ A.
An exact proof term for the current goal is (setminusE1 (U ∩ A) {x} z HzF).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U A z HzUA).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
An exact proof term for the current goal is (HUsubX z HzU).
We prove the intermediate claim HFclosed: closed_in X Tx F.
An exact proof term for the current goal is (Hfinite_closed F HFsubX HFfin).
We prove the intermediate claim HXFopen: open_in X Tx (X ∖ F).
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFclosed).
We prove the intermediate claim HXF: X ∖ F ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (X ∖ F ∈ Tx) HXFopen).
Set V to be the term U ∩ (X ∖ F).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U (X ∖ F) Htop HU HXF).
We prove the intermediate claim HxnotF: x ∉ F.
Assume HxF: x ∈ F.
We prove the intermediate claim HxnotSing: x ∉ {x}.
An exact proof term for the current goal is (setminusE2 (U ∩ A) {x} x HxF).
An exact proof term for the current goal is (HxnotSing (SingI x)).
We prove the intermediate claim HxXF: x ∈ X ∖ F.
An exact proof term for the current goal is (setminusI X F x HxX HxnotF).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectI U (X ∖ F) x HxU HxXF).
Apply (Hnbr V HV HxV) to the current goal.
Let y be given.
Assume Hyconj: y ∈ A ∧ y ≠ x ∧ y ∈ V.
We prove the intermediate claim HyAneq: y ∈ A ∧ y ≠ x.
An exact proof term for the current goal is (andEL (y ∈ A ∧ y ≠ x) (y ∈ V) Hyconj).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (andEL (y ∈ A) (y ≠ x) HyAneq).
We prove the intermediate claim Hyneq: y ≠ x.
An exact proof term for the current goal is (andER (y ∈ A) (y ≠ x) HyAneq).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (y ∈ A ∧ y ≠ x) (y ∈ V) Hyconj).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (X ∖ F) y HyV).
We prove the intermediate claim HyXF: y ∈ X ∖ F.
An exact proof term for the current goal is (binintersectE2 U (X ∖ F) y HyV).
We prove the intermediate claim HyNotF: y ∉ F.
An exact proof term for the current goal is (setminusE2 X F y HyXF).
We prove the intermediate claim HyUA: y ∈ U ∩ A.
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
We prove the intermediate claim HyNotSing: y ∉ {x}.
Assume HySing: y ∈ {x}.
We prove the intermediate claim Hyeq: y = x.
An exact proof term for the current goal is (SingE x y HySing).
An exact proof term for the current goal is (Hyneq Hyeq).
We prove the intermediate claim HyF: y ∈ F.
An exact proof term for the current goal is (setminusI (U ∩ A) {x} y HyUA HyNotSing).
An exact proof term for the current goal is (HyNotF HyF).
Assume HxnotA: x ∉ A.
Set F to be the term U ∩ A.
We prove the intermediate claim HFsubX: F ⊆ X.
Let z be given.
Assume HzF: z ∈ F.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U A z HzF).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
An exact proof term for the current goal is (HUsubX z HzU).
We prove the intermediate claim HFclosed: closed_in X Tx F.
An exact proof term for the current goal is (Hfinite_closed F HFsubX Hfin).
We prove the intermediate claim HXFopen: open_in X Tx (X ∖ F).
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFclosed).
We prove the intermediate claim HXF: X ∖ F ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (X ∖ F ∈ Tx) HXFopen).
Set V to be the term U ∩ (X ∖ F).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U (X ∖ F) Htop HU HXF).
We prove the intermediate claim HxnotF: x ∉ F.
Assume HxF: x ∈ F.
We prove the intermediate claim HxA': x ∈ A.
An exact proof term for the current goal is (binintersectE2 U A x HxF).
An exact proof term for the current goal is (HxnotA HxA').
We prove the intermediate claim HxXF: x ∈ X ∖ F.
An exact proof term for the current goal is (setminusI X F x HxX HxnotF).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectI U (X ∖ F) x HxU HxXF).
Apply (Hnbr V HV HxV) to the current goal.
Let y be given.
Assume Hyconj: y ∈ A ∧ y ≠ x ∧ y ∈ V.
We prove the intermediate claim HyAneq: y ∈ A ∧ y ≠ x.
An exact proof term for the current goal is (andEL (y ∈ A ∧ y ≠ x) (y ∈ V) Hyconj).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (andEL (y ∈ A) (y ≠ x) HyAneq).
We prove the intermediate claim Hyneq: y ≠ x.
An exact proof term for the current goal is (andER (y ∈ A) (y ≠ x) HyAneq).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (andER (y ∈ A ∧ y ≠ x) (y ∈ V) Hyconj).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (X ∖ F) y HyV).
We prove the intermediate claim HyXF: y ∈ X ∖ F.
An exact proof term for the current goal is (binintersectE2 U (X ∖ F) y HyV).
We prove the intermediate claim HyNotF: y ∉ F.
An exact proof term for the current goal is (setminusE2 X F y HyXF).
We prove the intermediate claim HyF: y ∈ F.
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
An exact proof term for the current goal is (HyNotF HyF).
Assume Hinf: ∀U ∈ Tx, x ∈ U → infinite (U ∩ A).
We will prove limit_point_of X Tx A x.
We will prove topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HinfUA: infinite (U ∩ A).
An exact proof term for the current goal is (Hinf U HU HxU).
We prove the intermediate claim Hnotfin: ¬ finite (U ∩ A).
An exact proof term for the current goal is HinfUA.
Apply (xm (∃y : set, y ∈ U ∩ A ∧ y ≠ x)) to the current goal.
Assume Hex.
Apply Hex to the current goal.
Let y be given.
Assume Hypair.
We use y to witness the existential quantifier.
We prove the intermediate claim HyUA: y ∈ U ∩ A.
An exact proof term for the current goal is (andEL (y ∈ U ∩ A) (y ≠ x) Hypair).
We prove the intermediate claim Hyneq: y ≠ x.
An exact proof term for the current goal is (andER (y ∈ U ∩ A) (y ≠ x) Hypair).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y HyUA).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y HyUA).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is Hyneq.
An exact proof term for the current goal is HyU.
Assume Hno: ¬ (∃y : set, y ∈ U ∩ A ∧ y ≠ x).
We prove the intermediate claim HsubSing: U ∩ A ⊆ {x}.
Let y be given.
Assume HyUA: y ∈ U ∩ A.
Apply (xm (y = x)) to the current goal.
Assume Heq: y = x.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI x).
Assume Hneq: ¬ (y = x).
Apply FalseE to the current goal.
Apply Hno to the current goal.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HyUA.
Assume Heq: y = x.
An exact proof term for the current goal is (Hneq Heq).
We prove the intermediate claim HfinUA: finite (U ∩ A).
An exact proof term for the current goal is (Subq_finite {x} (Sing_finite x) (U ∩ A) HsubSing).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnotfin HfinUA).
∎