Let X, Tx, Y and A be given.
Assume HTx: topology_on X Tx.
Assume HY: closed_in X Tx Y.
Assume HA: closed_in Y (subspace_topology X Tx Y) A.
We will prove closed_in X Tx A.
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (andEL (Y ⊆ X) (∃U ∈ Tx, Y = X ∖ U) (andER (topology_on X Tx) (Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U) HY)).
We prove the intermediate claim Hexists: ∃C : set, closed_in X Tx C ∧ A = C ∩ Y.
Apply (iffEL (closed_in Y (subspace_topology X Tx Y) A) (∃C : set, closed_in X Tx C ∧ A = C ∩ Y) (closed_in_subspace_iff_intersection X Tx Y A HTx HYsub)) to the current goal.
An exact proof term for the current goal is HA.
Apply Hexists to the current goal.
Let C be given.
Assume HCandA: closed_in X Tx C ∧ A = C ∩ Y.
We prove the intermediate claim HCclosed: closed_in X Tx C.
An exact proof term for the current goal is (andEL (closed_in X Tx C) (A = C ∩ Y) HCandA).
We prove the intermediate claim HAeq: A = C ∩ Y.
An exact proof term for the current goal is (andER (closed_in X Tx C) (A = C ∩ Y) HCandA).
We prove the intermediate claim HCexists: ∃U ∈ Tx, C = X ∖ U.
An exact proof term for the current goal is (andER (C ⊆ X) (∃U ∈ Tx, C = X ∖ U) (andER (topology_on X Tx) (C ⊆ X ∧ ∃U ∈ Tx, C = X ∖ U) HCclosed)).
Apply HCexists to the current goal.
Let U be given.
Assume HU: U ∈ Tx ∧ C = X ∖ U.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (C = X ∖ U) HU).
We prove the intermediate claim HCeq: C = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (C = X ∖ U) HU).
We prove the intermediate claim HYexists: ∃V ∈ Tx, Y = X ∖ V.
An exact proof term for the current goal is (andER (Y ⊆ X) (∃V ∈ Tx, Y = X ∖ V) (andER (topology_on X Tx) (Y ⊆ X ∧ ∃V ∈ Tx, Y = X ∖ V) HY)).
Apply HYexists to the current goal.
Let V be given.
Assume HV: V ∈ Tx ∧ Y = X ∖ V.
We prove the intermediate claim HVinTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (Y = X ∖ V) HV).
We prove the intermediate claim HYeq: Y = X ∖ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (Y = X ∖ V) HV).
We prove the intermediate claim HAeqSetminus: A = (X ∖ U) ∩ (X ∖ V).
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HCeq (from left to right).
rewrite the current goal using HYeq (from left to right).
Use reflexivity.
We prove the intermediate claim HDeM: (X ∖ U) ∩ (X ∖ V) = X ∖ (U ∪ V).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ U) ∩ (X ∖ V).
We will prove x ∈ X ∖ (U ∪ V).
We prove the intermediate claim HxXU: x ∈ X ∖ U.
An exact proof term for the current goal is (binintersectE1 (X ∖ U) (X ∖ V) x Hx).
We prove the intermediate claim HxXV: x ∈ X ∖ V.
An exact proof term for the current goal is (binintersectE2 (X ∖ U) (X ∖ V) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X U x HxXU).
We prove the intermediate claim HxninU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxXU).
We prove the intermediate claim HxninV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxXV).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxUV: x ∈ U ∪ V.
We will prove False.
Apply (binunionE U V x HxUV) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (HxninU HxU).
Assume HxV: x ∈ V.
An exact proof term for the current goal is (HxninV HxV).
Let x be given.
Assume Hx: x ∈ X ∖ (U ∪ V).
We will prove x ∈ (X ∖ U) ∩ (X ∖ V).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (U ∪ V) x Hx).
We prove the intermediate claim HxninUV: x ∉ U ∪ V.
An exact proof term for the current goal is (setminusE2 X (U ∪ V) x Hx).
Apply binintersectI to the current goal.
We will prove x ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxU: x ∈ U.
We will prove False.
We prove the intermediate claim HxUV: x ∈ U ∪ V.
An exact proof term for the current goal is (binunionI1 U V x HxU).
An exact proof term for the current goal is (HxninUV HxUV).
We will prove x ∈ X ∖ V.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxV: x ∈ V.
We will prove False.
We prove the intermediate claim HxUV: x ∈ U ∪ V.
An exact proof term for the current goal is (binunionI2 U V x HxV).
An exact proof term for the current goal is (HxninUV HxUV).
We prove the intermediate claim HUV: U ∪ V ∈ Tx.
An exact proof term for the current goal is (lemma_union_two_open X Tx U V HTx HUinTx HVinTx).
We prove the intermediate claim HAeqFinal: A = X ∖ (U ∪ V).
rewrite the current goal using HAeqSetminus (from left to right).
An exact proof term for the current goal is HDeM.
We will prove topology_on X Tx ∧ (A ⊆ X ∧ ∃U0 ∈ Tx, A = X ∖ U0).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
We will prove A ⊆ X.
rewrite the current goal using HAeqFinal (from left to right).
An exact proof term for the current goal is (setminus_Subq X (U ∪ V)).
We will prove ∃U0 ∈ Tx, A = X ∖ U0.
We use (U ∪ V) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUV.
An exact proof term for the current goal is HAeqFinal.
∎