Let X, Tx, U and A be given.
Assume Htop: topology_on X Tx.
Assume HU: open_in X Tx U.
Assume HA: closed_in X Tx A.
We will prove open_in X Tx (U ∖ A) ∧ closed_in X Tx (A ∖ U).
We prove the intermediate claim HUtop: U ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (U ∈ Tx) HU).
We prove the intermediate claim HAdef: A ⊆ X ∧ (∃V ∈ Tx, A = X ∖ V).
An exact proof term for the current goal is (andER (topology_on X Tx) (A ⊆ X ∧ (∃V ∈ Tx, A = X ∖ V)) HA).
We prove the intermediate claim HexV: ∃V ∈ Tx, A = X ∖ V.
An exact proof term for the current goal is (andER (A ⊆ X) (∃V ∈ Tx, A = X ∖ V) HAdef).
Apply HexV to the current goal.
Let V be given.
Assume HVandEq.
Apply HVandEq to the current goal.
Assume HV: V ∈ Tx.
Assume HAeq: A = X ∖ V.
Apply andI to the current goal.
We will prove open_in X Tx (U ∖ A).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U Htop HUtop).
We prove the intermediate claim HUminusA_eq_UinterV: U ∖ A = U ∩ V.
rewrite the current goal using HAeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∖ (X ∖ V).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (setminusE1 U (X ∖ V) x Hx).
We prove the intermediate claim HxnotXV: x ∉ X ∖ V.
An exact proof term for the current goal is (setminusE2 U (X ∖ V) x Hx).
We prove the intermediate claim HxV: x ∈ V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x HxU).
Apply xm (x ∈ V) to the current goal.
Assume Hv.
An exact proof term for the current goal is Hv.
Assume Hnv.
Apply FalseE to the current goal.
Apply HxnotXV to the current goal.
An exact proof term for the current goal is (setminusI X V x HxX Hnv).
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
Let x be given.
Assume Hx: x ∈ U ∩ V.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x Hx).
We prove the intermediate claim HxnotXV: x ∉ X ∖ V.
Assume H.
Apply (setminusE2 X V x H) to the current goal.
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is (setminusI U (X ∖ V) x HxU HxnotXV).
rewrite the current goal using HUminusA_eq_UinterV (from left to right).
We prove the intermediate claim HUinterV: U ∩ V ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U V Htop HUtop HV).
An exact proof term for the current goal is (andI (topology_on X Tx) (U ∩ V ∈ Tx) Htop HUinterV).
We will prove closed_in X Tx (A ∖ U).
We prove the intermediate claim HAsub: A ⊆ X.
An exact proof term for the current goal is (andEL (A ⊆ X) (∃V0 ∈ Tx, A = X ∖ V0) HAdef).
We prove the intermediate claim HAminusU_sub: A ∖ U ⊆ X.
Let x be given.
Assume Hx.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (setminusE1 A U x Hx).
An exact proof term for the current goal is (HAsub x HxA).
We prove the intermediate claim HVU: V ∪ U ∈ Tx.
An exact proof term for the current goal is (lemma_union_two_open X Tx V U Htop HV HUtop).
We prove the intermediate claim HAminusU_eq_XminusVU: A ∖ U = X ∖ (V ∪ U).
rewrite the current goal using HAeq (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ V) ∖ U.
We prove the intermediate claim HxXV: x ∈ X ∖ V.
An exact proof term for the current goal is (setminusE1 (X ∖ V) U x Hx).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 (X ∖ V) U x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X V x HxXV).
We prove the intermediate claim HxnotV: x ∉ V.
An exact proof term for the current goal is (setminusE2 X V x HxXV).
We prove the intermediate claim HxnotVU: x ∉ V ∪ U.
Assume H.
Apply (binunionE V U x H) to the current goal.
Assume HxV.
An exact proof term for the current goal is (HxnotV HxV).
Assume HxU.
An exact proof term for the current goal is (HxnotU HxU).
An exact proof term for the current goal is (setminusI X (V ∪ U) x HxX HxnotVU).
Let x be given.
Assume Hx: x ∈ X ∖ (V ∪ U).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (V ∪ U) x Hx).
We prove the intermediate claim HxnotVU: x ∉ V ∪ U.
An exact proof term for the current goal is (setminusE2 X (V ∪ U) x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
Assume HxV.
Apply HxnotVU to the current goal.
An exact proof term for the current goal is (binunionI1 V U x HxV).
We prove the intermediate claim HxnotU: x ∉ U.
Assume HxU.
Apply HxnotVU to the current goal.
An exact proof term for the current goal is (binunionI2 V U x HxU).
We prove the intermediate claim HxXV: x ∈ X ∖ V.
An exact proof term for the current goal is (setminusI X V x HxX HxnotV).
An exact proof term for the current goal is (setminusI (X ∖ V) U x HxXV HxnotU).
We prove the intermediate claim HPred: ∃W ∈ Tx, A ∖ U = X ∖ W.
We use (V ∪ U) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HVU.
An exact proof term for the current goal is HAminusU_eq_XminusVU.
An exact proof term for the current goal is (andI (topology_on X Tx) (A ∖ U ⊆ X ∧ (∃W ∈ Tx, A ∖ U = X ∖ W)) Htop (andI (A ∖ U ⊆ X) (∃W ∈ Tx, A ∖ U = X ∖ W) HAminusU_sub HPred)).
∎