Let X, T, C and D be given.
Assume HC: closed_in X T C.
Assume HD: closed_in X T D.
We will prove closed_in X T (C ∩ D).
We prove the intermediate claim HTx: topology_on X T.
An exact proof term for the current goal is (closed_in_topology X T C HC).
We prove the intermediate claim HexU: ∃U ∈ T, C = X ∖ U.
An exact proof term for the current goal is (closed_in_exists_open_complement X T C HC).
We prove the intermediate claim HexV: ∃V ∈ T, D = X ∖ V.
An exact proof term for the current goal is (closed_in_exists_open_complement X T D HD).
Apply HexU to the current goal.
Let U be given.
Assume HUcore.
Apply HUcore to the current goal.
Assume HU: U ∈ T.
Assume HCe: C = X ∖ U.
Apply HexV to the current goal.
Let V be given.
Assume HVcore.
Apply HVcore to the current goal.
Assume HV: V ∈ T.
Assume HDe: D = X ∖ V.
Set UV to be the term ⋃ {U,V}.
We prove the intermediate claim Hpairsub: {U,V} ⊆ T.
Let W be given.
Assume HW: W ∈ {U,V}.
We prove the intermediate claim Hor: W = U ∨ W = V.
An exact proof term for the current goal is (UPairE W U V HW).
Apply Hor to the current goal.
Assume HWU: W = U.
rewrite the current goal using HWU (from left to right).
An exact proof term for the current goal is HU.
Assume HWV: W = V.
rewrite the current goal using HWV (from left to right).
An exact proof term for the current goal is HV.
We prove the intermediate claim HUVinT: UV ∈ T.
An exact proof term for the current goal is (topology_union_closed X T {U,V} HTx Hpairsub).
We prove the intermediate claim HUVeq: UV = U ∪ V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ UV.
Apply (UnionE_impred {U,V} x Hx) to the current goal.
Let Z be given.
Assume HxZ: x ∈ Z.
Assume HZ: Z ∈ {U,V}.
We prove the intermediate claim Hor: Z = U ∨ Z = V.
An exact proof term for the current goal is (UPairE Z U V HZ).
Apply Hor to the current goal.
Assume HZU: Z = U.
We prove the intermediate claim HxU: x ∈ U.
rewrite the current goal using HZU (from right to left).
An exact proof term for the current goal is HxZ.
An exact proof term for the current goal is (binunionI1 U V x HxU).
Assume HZV: Z = V.
We prove the intermediate claim HxV: x ∈ V.
rewrite the current goal using HZV (from right to left).
An exact proof term for the current goal is HxZ.
An exact proof term for the current goal is (binunionI2 U V x HxV).
Let x be given.
Assume Hx: x ∈ U ∪ V.
Apply (binunionE U V x Hx) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (UnionI {U,V} x U HxU (UPairI1 U V)).
Assume HxV: x ∈ V.
An exact proof term for the current goal is (UnionI {U,V} x V HxV (UPairI2 U V)).
We prove the intermediate claim Hsubset: (C ∩ D) ⊆ X.
Let x be given.
Assume Hx: x ∈ C ∩ D.
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (binintersectE1 C D x Hx).
An exact proof term for the current goal is (closed_in_subset X T C HC x HxC).
We prove the intermediate claim Heq: (C ∩ D) = X ∖ UV.
rewrite the current goal using HCe (from left to right).
rewrite the current goal using HDe (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ U) ∩ (X ∖ V).
We will prove x ∈ X ∖ UV.
We prove the intermediate claim HxU: x ∈ X ∖ U.
An exact proof term for the current goal is (binintersectE1 (X ∖ U) (X ∖ V) x Hx).
We prove the intermediate claim HxV: 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 HxU).
We prove the intermediate claim HxNotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxU).
We prove the intermediate claim HxNotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxV).
We prove the intermediate claim HxNotUV: x ∉ UV.
Assume HxUV: x ∈ UV.
Apply (UnionE_impred {U,V} x HxUV) to the current goal.
Let Z be given.
Assume HxZ: x ∈ Z.
Assume HZ: Z ∈ {U,V}.
We prove the intermediate claim Hor: Z = U ∨ Z = V.
An exact proof term for the current goal is (UPairE Z U V HZ).
Apply Hor to the current goal.
Assume HZU: Z = U.
We prove the intermediate claim HxU2: x ∈ U.
rewrite the current goal using HZU (from right to left).
An exact proof term for the current goal is HxZ.
An exact proof term for the current goal is (HxNotU HxU2).
Assume HZV: Z = V.
We prove the intermediate claim HxV2: x ∈ V.
rewrite the current goal using HZV (from right to left).
An exact proof term for the current goal is HxZ.
An exact proof term for the current goal is (HxNotV HxV2).
An exact proof term for the current goal is (setminusI X UV x HxX HxNotUV).
Let x be given.
Assume Hx: x ∈ X ∖ UV.
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 UV x Hx).
We prove the intermediate claim HxNotUV: x ∉ UV.
An exact proof term for the current goal is (setminusE2 X UV x Hx).
We prove the intermediate claim HxNotU: x ∉ U.
Assume HxU: x ∈ U.
We prove the intermediate claim HxUV: x ∈ UV.
An exact proof term for the current goal is (UnionI {U,V} x U HxU (UPairI1 U V)).
An exact proof term for the current goal is (HxNotUV HxUV).
We prove the intermediate claim HxNotV: x ∉ V.
Assume HxV: x ∈ V.
We prove the intermediate claim HxUV: x ∈ UV.
An exact proof term for the current goal is (UnionI {U,V} x V HxV (UPairI2 U V)).
An exact proof term for the current goal is (HxNotUV HxUV).
Apply binintersectI to the current goal.
An exact proof term for the current goal is (setminusI X U x HxX HxNotU).
An exact proof term for the current goal is (setminusI X V x HxX HxNotV).
Apply (closed_inI X T (C ∩ D)) to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is Hsubset.
We use UV to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUVinT.
An exact proof term for the current goal is Heq.
∎