Let X, Tx and A be given.
Assume HTx: topology_on X Tx.
Assume HA: A ⊆ X.
We will prove closure_of X Tx A = A ∪ limit_points_of X Tx A.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
We will prove x ∈ A ∪ limit_points_of X Tx A.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
Apply binunionI1 to the current goal.
An exact proof term for the current goal is HxA.
Assume HxnotA: x ∉ A.
Apply binunionI2 to the current goal.
We will prove x ∈ limit_points_of X Tx A.
We will prove x ∈ {y ∈ X|limit_point_of X Tx A y}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (closure_in_space X Tx A HTx x Hx).
We prove the intermediate claim Hcond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
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 HTx.
An exact proof term for the current goal is HxX.
We will prove ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
We prove the intermediate claim HUne: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim Hexists: ∃y : set, y ∈ U ∩ A.
Apply (xm (∃y : set, y ∈ U ∩ A)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hnoex: ¬ (∃y : set, y ∈ U ∩ A).
Apply FalseE to the current goal.
Apply HUne to the current goal.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
Apply FalseE to the current goal.
Apply Hnoex to the current goal.
We use y to witness the existential quantifier.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is (Subq_Empty (U ∩ A)).
Apply Hexists to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ A.
We use y to witness the existential quantifier.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U A y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 U A y Hy).
We will prove 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 HyA.
We will prove y ≠ x.
Assume Heq: y = x.
Apply HxnotA to the current goal.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyA.
An exact proof term for the current goal is HyU.
Let x be given.
Assume Hx: x ∈ A ∪ limit_points_of X Tx A.
We will prove x ∈ closure_of X Tx A.
Apply (binunionE A (limit_points_of X Tx A) x Hx) to the current goal.
Assume HxA: x ∈ A.
Apply (xm (x ∈ X)) to the current goal.
Assume HxX: x ∈ X.
We will prove x ∈ {y ∈ X|∀U : set, U ∈ Tx → y ∈ U → U ∩ A ≠ Empty}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
Assume Hempty: U ∩ A = Empty.
We prove the intermediate claim HxUA: x ∈ U ∩ A.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HxA.
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HxUA.
An exact proof term for the current goal is (EmptyE x HxEmpty).
Assume HxnotX: x ∉ X.
Apply FalseE to the current goal.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
An exact proof term for the current goal is (HxnotX HxX).
Assume Hxlim: x ∈ limit_points_of X Tx A.
We prove the intermediate claim Hlimparts: x ∈ X ∧ limit_point_of X Tx A x.
An exact proof term for the current goal is (SepE X (λy ⇒ limit_point_of X Tx A y) x Hxlim).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (limit_point_of X Tx A x) Hlimparts).
We prove the intermediate claim Hlim: limit_point_of X Tx A x.
An exact proof term for the current goal is (andER (x ∈ X) (limit_point_of X Tx A x) Hlimparts).
We prove the intermediate claim Hlim_cond: ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
We prove the intermediate claim Hlim_full: topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
An exact proof term for the current goal is Hlim.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U) Hlim_full).
We will prove x ∈ {y ∈ X|∀U : set, U ∈ Tx → y ∈ U → U ∩ A ≠ Empty}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ A ≠ Empty.
We prove the intermediate claim Hexists: ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.
An exact proof term for the current goal is (Hlim_cond U HU HxU).
Apply Hexists to the current goal.
Let y be given.
Assume Hy_parts: y ∈ A ∧ y ≠ x ∧ y ∈ U.
We prove the intermediate claim Hy_left: y ∈ A ∧ y ≠ x.
An exact proof term for the current goal is (andEL (y ∈ A ∧ y ≠ x) (y ∈ U) Hy_parts).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (andEL (y ∈ A) (y ≠ x) Hy_left).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (andER (y ∈ A ∧ y ≠ x) (y ∈ U) Hy_parts).
Assume Heq: U ∩ A = Empty.
We prove the intermediate claim HyUA: y ∈ U ∩ A.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HyU.
An exact proof term for the current goal is HyA.
We prove the intermediate claim HyEmpty: y ∈ Empty.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HyUA.
An exact proof term for the current goal is (EmptyE y HyEmpty).
∎