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 W to be the term U ∩ V.
We prove the intermediate claim HW: W ∈ T.
An exact proof term for the current goal is (topology_binintersect_closed X T U V HTx HU HV).
We prove the intermediate claim Hsubset: (C ∪ D) ⊆ X.
Let x be given.
Assume Hx: x ∈ C ∪ D.
Apply (binunionE C D x Hx) to the current goal.
Assume HxC: x ∈ C.
An exact proof term for the current goal is (closed_in_subset X T C HC x HxC).
Assume HxD: x ∈ D.
An exact proof term for the current goal is (closed_in_subset X T D HD x HxD).
We prove the intermediate claim Heq: (C ∪ D) = X ∖ W.
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 ∖ W.
Apply (binunionE (X ∖ U) (X ∖ V) x Hx) to the current goal.
Assume HxU: x ∈ X ∖ U.
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 HxNotW: x ∉ W.
Assume HxW: x ∈ W.
We prove the intermediate claim HxUin: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x HxW).
An exact proof term for the current goal is (HxNotU HxUin).
An exact proof term for the current goal is (setminusI X W x HxX HxNotW).
Assume HxV: x ∈ X ∖ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X V x HxV).
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 HxNotW: x ∉ W.
Assume HxW: x ∈ W.
We prove the intermediate claim HxVin: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x HxW).
An exact proof term for the current goal is (HxNotV HxVin).
An exact proof term for the current goal is (setminusI X W x HxX HxNotW).
Let x be given.
Assume Hx: x ∈ X ∖ W.
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 W x Hx).
We prove the intermediate claim HxNotW: x ∉ W.
An exact proof term for the current goal is (setminusE2 X W x Hx).
Apply (xm (x ∈ U)) to the current goal.
Assume HxUin: x ∈ U.
We prove the intermediate claim HxNotV: x ∉ V.
Assume HxVin: x ∈ V.
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectI U V x HxUin HxVin).
An exact proof term for the current goal is (HxNotW HxW).
An exact proof term for the current goal is (binunionI2 (X ∖ U) (X ∖ V) x (setminusI X V x HxX HxNotV)).
Assume HxNotU: ¬ (x ∈ U).
An exact proof term for the current goal is (binunionI1 (X ∖ U) (X ∖ V) x (setminusI X U x HxX HxNotU)).
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 W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HW.
An exact proof term for the current goal is Heq.
∎