Let X, Tx and A be given.
Assume Htop: topology_on X Tx.
We will prove closure_of X Tx (closure_of X Tx A) = closure_of X Tx A ∧ closed_in X Tx (closure_of X Tx A).
Set clA to be the term closure_of X Tx A.
We prove the intermediate claim HclA_sub: clA ⊆ X.
Let x be given.
Assume Hx: x ∈ clA.
We will prove 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 andI to the current goal.
We will prove closure_of X Tx clA = clA.
We prove the intermediate claim HclA_closed: closed_in X Tx clA.
We prove the intermediate claim HAX_sub: A ∩ X ⊆ X.
An exact proof term for the current goal is (binintersect_Subq_2 A X).
We prove the intermediate claim Heq_closure: closure_of X Tx (A ∩ X) = closure_of X Tx A.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (A ∩ X).
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 (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x Hx).
We prove the intermediate claim Hcond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (A ∩ X) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x Hx).
We prove the intermediate claim Hpred: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HUX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim Hinter1: U ∩ (A ∩ X) ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim Heq_inter: U ∩ (A ∩ X) = U ∩ A.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ X).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ X) y Hy).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectE2 U (A ∩ X) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A X y HyAX).
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
Let y be given.
Assume Hy: y ∈ U ∩ A.
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 prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUX y HyU).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectI A X y HyA HyX).
An exact proof term for the current goal is (binintersectI U (A ∩ X) y HyU HyAX).
rewrite the current goal using Heq_inter (from right to left).
An exact proof term for the current goal is Hinter1.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hpred).
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
We will prove x ∈ closure_of X Tx (A ∩ X).
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).
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).
We prove the intermediate claim Hpred: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (A ∩ X) ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HUX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim Hinter1: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim Heq_inter: U ∩ (A ∩ X) = U ∩ A.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ X).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ X) y Hy).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectE2 U (A ∩ X) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A X y HyAX).
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
Let y be given.
Assume Hy: y ∈ U ∩ A.
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 prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUX y HyU).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectI A X y HyA HyX).
An exact proof term for the current goal is (binintersectI U (A ∩ X) y HyU HyAX).
rewrite the current goal using Heq_inter (from left to right).
An exact proof term for the current goal is Hinter1.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x HxX Hpred).
rewrite the current goal using Heq_closure (from right to left).
An exact proof term for the current goal is (closure_is_closed X Tx (A ∩ X) Htop HAX_sub).
An exact proof term for the current goal is (closed_closure_eq X Tx clA Htop HclA_closed).
We will prove closed_in X Tx clA.
We prove the intermediate claim HAX_sub: A ∩ X ⊆ X.
An exact proof term for the current goal is (binintersect_Subq_2 A X).
We prove the intermediate claim Heq_closure: closure_of X Tx (A ∩ X) = closure_of X Tx A.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X Tx (A ∩ X).
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 (SepE1 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x Hx).
We prove the intermediate claim Hcond: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (A ∩ X) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x Hx).
We prove the intermediate claim Hpred: ∀U : set, U ∈ Tx → x ∈ U → U ∩ A ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HUX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim Hinter1: U ∩ (A ∩ X) ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim Heq_inter: U ∩ (A ∩ X) = U ∩ A.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ X).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ X) y Hy).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectE2 U (A ∩ X) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A X y HyAX).
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
Let y be given.
Assume Hy: y ∈ U ∩ A.
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 prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUX y HyU).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectI A X y HyA HyX).
An exact proof term for the current goal is (binintersectI U (A ∩ X) y HyU HyAX).
rewrite the current goal using Heq_inter (from right to left).
An exact proof term for the current goal is Hinter1.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ A ≠ Empty) x HxX Hpred).
Let x be given.
Assume Hx: x ∈ closure_of X Tx A.
We will prove x ∈ closure_of X Tx (A ∩ X).
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).
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).
We prove the intermediate claim Hpred: ∀U : set, U ∈ Tx → x ∈ U → U ∩ (A ∩ X) ≠ Empty.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HUX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HU).
We prove the intermediate claim Hinter1: U ∩ A ≠ Empty.
An exact proof term for the current goal is (Hcond U HU HxU).
We prove the intermediate claim Heq_inter: U ∩ (A ∩ X) = U ∩ A.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ (A ∩ X).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U (A ∩ X) y Hy).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectE2 U (A ∩ X) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE1 A X y HyAX).
An exact proof term for the current goal is (binintersectI U A y HyU HyA).
Let y be given.
Assume Hy: y ∈ U ∩ A.
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 prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HUX y HyU).
We prove the intermediate claim HyAX: y ∈ A ∩ X.
An exact proof term for the current goal is (binintersectI A X y HyA HyX).
An exact proof term for the current goal is (binintersectI U (A ∩ X) y HyU HyAX).
rewrite the current goal using Heq_inter (from left to right).
An exact proof term for the current goal is Hinter1.
An exact proof term for the current goal is (SepI X (λx0 ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ (A ∩ X) ≠ Empty) x HxX Hpred).
rewrite the current goal using Heq_closure (from right to left).
An exact proof term for the current goal is (closure_is_closed X Tx (A ∩ X) Htop HAX_sub).
∎