Let X, Tx and A be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
We will prove closed_in X Tx (closure_of X Tx A).
We will prove topology_on X Tx ∧ (closure_of X Tx A ⊆ X ∧ ∃U ∈ Tx, closure_of X Tx A = X ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
We will prove closure_of X Tx A ⊆ X ∧ ∃U ∈ Tx, closure_of X Tx A = X ∖ U.
Apply andI to the current goal.
We will prove closure_of X Tx A ⊆ X.
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
Set Complement to be the term X ∖ closure_of X Tx A.
Set OpenFamily to be the term {U ∈ Tx|U ∩ A = Empty}.
We prove the intermediate claim Hcomp_eq: Complement = ⋃ OpenFamily.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Complement.
We will prove x ∈ ⋃ OpenFamily.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (closure_of X Tx A) x Hx).
We prove the intermediate claim Hxnotcl: x ∉ closure_of X Tx A.
An exact proof term for the current goal is (setminusE2 X (closure_of X Tx A) x Hx).
We prove the intermediate claim Hexists: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ∩ A = Empty.
An exact proof term for the current goal is (not_in_closure_has_disjoint_open X Tx A x Htop HA HxX Hxnotcl).
Apply Hexists to the current goal.
Let U be given.
Assume HU_parts.
We prove the intermediate claim HU_and_xU: U ∈ Tx ∧ x ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (U ∩ A = Empty) HU_parts).
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HU_and_xU).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HU_and_xU).
We prove the intermediate claim HUdisj: U ∩ A = Empty.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (U ∩ A = Empty) HU_parts).
We prove the intermediate claim HUinFam: U ∈ OpenFamily.
An exact proof term for the current goal is (SepI Tx (λV ⇒ V ∩ A = Empty) U HU HUdisj).
An exact proof term for the current goal is (UnionI OpenFamily x U HxU HUinFam).
Let x be given.
Assume Hx: x ∈ ⋃ OpenFamily.
We will prove x ∈ Complement.
Apply (UnionE_impred OpenFamily x Hx) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HUFam: U ∈ OpenFamily.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (SepE1 Tx (λV ⇒ V ∩ A = Empty) U HUFam).
We prove the intermediate claim HUdisj: U ∩ A = Empty.
An exact proof term for the current goal is (SepE2 Tx (λV ⇒ V ∩ A = Empty) U HUFam).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x HxU).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hxcl: x ∈ closure_of X Tx A.
We prove the intermediate claim Hcond: ∀V : set, V ∈ Tx → x ∈ V → V ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λy ⇒ ∀V : set, V ∈ Tx → y ∈ V → V ∩ A ≠ Empty) x Hxcl).
We prove the intermediate claim Hcontra: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
An exact proof term for the current goal is (Hcontra HUdisj).
We prove the intermediate claim Hopen_subset: OpenFamily ⊆ Tx.
Let U be given.
Assume HU: U ∈ OpenFamily.
An exact proof term for the current goal is (SepE1 Tx (λV ⇒ V ∩ A = Empty) U HU).
We prove the intermediate claim Hcomp_open: Complement ∈ Tx.
rewrite the current goal using Hcomp_eq (from left to right).
An exact proof term for the current goal is (topology_union_closed X Tx OpenFamily Htop Hopen_subset).
We use Complement to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hcomp_open.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
We will prove x ∈ X ∖ Complement.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x Hx).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hxcomp: x ∈ Complement.
We prove the intermediate claim Hxnotcl: x ∉ closure_of X Tx A.
An exact proof term for the current goal is (setminusE2 X (closure_of X Tx A) x Hxcomp).
An exact proof term for the current goal is (Hxnotcl Hx).
Let x be given.
Assume Hx: x ∈ X ∖ Complement.
We will prove x ∈ closure_of X Tx A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X Complement x Hx).
We prove the intermediate claim Hxnotcomp: x ∉ Complement.
An exact proof term for the current goal is (setminusE2 X Complement x Hx).
Apply (xm (x ∈ closure_of X Tx A)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume Hxnotcl: x ∉ closure_of X Tx A.
Apply FalseE to the current goal.
Apply Hxnotcomp to the current goal.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is Hxnotcl.
∎