Let X, Tx and A be given.
Assume Htop: topology_on X Tx.
Assume HA: A ⊆ X.
We will prove interior_of X Tx A = X ∖ closure_of X Tx (X ∖ A).
We prove the intermediate claim HXA_sub: X ∖ A ⊆ X.
Let x be given.
Assume Hx: x ∈ X ∖ A.
An exact proof term for the current goal is (setminusE1 X A x Hx).
We prove the intermediate claim Hclosed: closed_in X Tx (closure_of X Tx (X ∖ A)).
An exact proof term for the current goal is (closure_is_closed X Tx (X ∖ A) Htop HXA_sub).
We prove the intermediate claim Hclosed_parts: topology_on X Tx ∧ (closure_of X Tx (X ∖ A) ⊆ X ∧ ∃U ∈ Tx, closure_of X Tx (X ∖ A) = X ∖ U).
An exact proof term for the current goal is Hclosed.
We prove the intermediate claim Hexists: ∃U ∈ Tx, closure_of X Tx (X ∖ A) = X ∖ U.
We prove the intermediate claim Hpart2: closure_of X Tx (X ∖ A) ⊆ X ∧ ∃U ∈ Tx, closure_of X Tx (X ∖ A) = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (closure_of X Tx (X ∖ A) ⊆ X ∧ ∃U ∈ Tx, closure_of X Tx (X ∖ A) = X ∖ U) Hclosed_parts).
An exact proof term for the current goal is (andER (closure_of X Tx (X ∖ A) ⊆ X) (∃U ∈ Tx, closure_of X Tx (X ∖ A) = X ∖ U) Hpart2).
Apply Hexists to the current goal.
Let U be given.
Assume HU_conj: U ∈ Tx ∧ closure_of X Tx (X ∖ A) = X ∖ U.
We prove the intermediate claim HU_open: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (closure_of X Tx (X ∖ A) = X ∖ U) HU_conj).
We prove the intermediate claim Heq_clXA: closure_of X Tx (X ∖ A) = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (closure_of X Tx (X ∖ A) = X ∖ U) HU_conj).
We prove the intermediate claim HcompU: X ∖ closure_of X Tx (X ∖ A) = U.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∖ closure_of X Tx (X ∖ A).
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X (closure_of X Tx (X ∖ A)) x Hx).
We prove the intermediate claim Hxnotcl: x ∉ closure_of X Tx (X ∖ A).
An exact proof term for the current goal is (setminusE2 X (closure_of X Tx (X ∖ A)) x Hx).
Apply (xm (x ∈ U)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HxnotU: x ∉ U.
Apply FalseE to the current goal.
Apply Hxnotcl to the current goal.
We prove the intermediate claim HxXminusU: x ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotU.
We will prove x ∈ closure_of X Tx (X ∖ A).
rewrite the current goal using Heq_clXA (from left to right).
An exact proof term for the current goal is HxXminusU.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ X ∖ closure_of X Tx (X ∖ 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 HU_open).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x Hx).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume Hxcl: x ∈ closure_of X Tx (X ∖ A).
We prove the intermediate claim HxXminusU: x ∈ X ∖ U.
rewrite the current goal using Heq_clXA (from right to left).
An exact proof term for the current goal is Hxcl.
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxXminusU).
An exact proof term for the current goal is (HxnotU Hx).
We prove the intermediate claim HUsub_A: U ⊆ A.
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ 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 HU_open).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x Hx).
Apply (xm (x ∈ A)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HxnotA: x ∉ A.
Apply FalseE to the current goal.
We prove the intermediate claim HxXminusA: x ∈ X ∖ A.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotA.
We prove the intermediate claim Hxincl: x ∈ closure_of X Tx (X ∖ A).
An exact proof term for the current goal is (subset_of_closure X Tx (X ∖ A) Htop HXA_sub x HxXminusA).
We prove the intermediate claim HxXminusU: x ∈ X ∖ U.
rewrite the current goal using Heq_clXA (from right to left).
An exact proof term for the current goal is Hxincl.
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxXminusU).
An exact proof term for the current goal is (HxnotU Hx).
We prove the intermediate claim Hint_eq_U: interior_of X Tx A = U.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ interior_of X Tx A.
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λy ⇒ ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ A) x Hx).
We prove the intermediate claim Hexists_V: ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ A.
An exact proof term for the current goal is (SepE2 X (λy ⇒ ∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ A) x Hx).
Apply Hexists_V to the current goal.
Let V be given.
Assume HV_conj.
We prove the intermediate claim HV_and_xV: V ∈ Tx ∧ x ∈ V.
An exact proof term for the current goal is (andEL (V ∈ Tx ∧ x ∈ V) (V ⊆ A) HV_conj).
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (x ∈ V) HV_and_xV).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andER (V ∈ Tx) (x ∈ V) HV_and_xV).
We prove the intermediate claim HVsub: V ⊆ A.
An exact proof term for the current goal is (andER (V ∈ Tx ∧ x ∈ V) (V ⊆ A) HV_conj).
Apply (xm (x ∈ U)) to the current goal.
Assume H.
An exact proof term for the current goal is H.
Assume HxnotU: x ∉ U.
Apply FalseE to the current goal.
We prove the intermediate claim HxXminusU: x ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxnotU.
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx (X ∖ A).
rewrite the current goal using Heq_clXA (from left to right).
An exact proof term for the current goal is HxXminusU.
We prove the intermediate claim Hcond: ∀W : set, W ∈ Tx → x ∈ W → W ∩ (X ∖ A) ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λy ⇒ ∀W : set, W ∈ Tx → y ∈ W → W ∩ (X ∖ A) ≠ Empty) x Hxcl).
We prove the intermediate claim HVmeets: V ∩ (X ∖ A) ≠ Empty.
An exact proof term for the current goal is (Hcond V HV HxV).
We prove the intermediate claim HVdisj: V ∩ (X ∖ A) = Empty.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ V ∩ (X ∖ A).
We will prove y ∈ Empty.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE1 V (X ∖ A) y Hy).
We prove the intermediate claim HyXminusA: y ∈ X ∖ A.
An exact proof term for the current goal is (binintersectE2 V (X ∖ A) y Hy).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (HVsub y HyV).
We prove the intermediate claim HynotA: y ∉ A.
An exact proof term for the current goal is (setminusE2 X A y HyXminusA).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HynotA HyA).
An exact proof term for the current goal is (Subq_Empty (V ∩ (X ∖ A))).
An exact proof term for the current goal is (HVmeets HVdisj).
Let x be given.
Assume Hx: x ∈ U.
We will prove x ∈ interior_of X Tx 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 HU_open).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsub x Hx).
We will prove x ∈ {y ∈ X|∃V : set, V ∈ Tx ∧ y ∈ V ∧ V ⊆ A}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove ∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ A.
We use U to witness the existential quantifier.
We will prove U ∈ Tx ∧ x ∈ U ∧ U ⊆ A.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU_open.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is HUsub_A.
We will prove interior_of X Tx A = X ∖ closure_of X Tx (X ∖ A).
rewrite the current goal using HcompU (from left to right).
An exact proof term for the current goal is Hint_eq_U.
∎