Let X, Tx, Y and A be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
We will prove closed_in Y (subspace_topology X Tx Y) A ↔ ∃C : set, closed_in X Tx C ∧ A = C ∩ Y.
Apply iffI to the current goal.
Assume HAclosed: closed_in Y (subspace_topology X Tx Y) A.
We will prove ∃C : set, closed_in X Tx C ∧ A = C ∩ Y.
We prove the intermediate claim HTsubspace: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HY).
We prove the intermediate claim HAdef: topology_on Y (subspace_topology X Tx Y) ∧ (A ⊆ Y ∧ ∃U ∈ subspace_topology X Tx Y, A = Y ∖ U).
An exact proof term for the current goal is HAclosed.
We prove the intermediate claim HAandEx: A ⊆ Y ∧ ∃U ∈ subspace_topology X Tx Y, A = Y ∖ U.
An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (A ⊆ Y ∧ ∃U ∈ subspace_topology X Tx Y, A = Y ∖ U) HAdef).
We prove the intermediate claim HexU: ∃U ∈ subspace_topology X Tx Y, A = Y ∖ U.
An exact proof term for the current goal is (andER (A ⊆ Y) (∃U ∈ subspace_topology X Tx Y, A = Y ∖ U) HAandEx).
Apply HexU to the current goal.
Let U be given.
Assume HandEq.
Apply HandEq to the current goal.
Assume HUsubspace: U ∈ subspace_topology X Tx Y.
Assume HAeq: A = Y ∖ U.
We prove the intermediate claim HUexV: ∃V ∈ Tx, U = V ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HUsubspace).
Apply HUexV to the current goal.
Let V be given.
Assume HVandEq.
Apply HVandEq to the current goal.
Assume HV: V ∈ Tx.
Assume HUeq: U = V ∩ Y.
Set C to be the term X ∖ V.
We prove the intermediate claim HCclosed: closed_in X Tx C.
We will prove topology_on X Tx ∧ (C ⊆ X ∧ ∃W ∈ Tx, C = X ∖ W).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Apply andI to the current goal.
An exact proof term for the current goal is (setminus_Subq X V).
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV.
Use reflexivity.
We prove the intermediate claim HAeqC: A = C ∩ Y.
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HUeq (from left to right).
We will prove Y ∖ (V ∩ Y) = (X ∖ V) ∩ Y.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Y ∖ (V ∩ Y).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (setminusE1 Y (V ∩ Y) x Hx).
We prove the intermediate claim HxnotVY: x ∉ V ∩ Y.
An exact proof term for the current goal is (setminusE2 Y (V ∩ Y) x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
Assume HxV: x ∈ V.
Apply HxnotVY to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HY x HxY).
Apply binintersectI to the current goal.
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 HxnotV.
An exact proof term for the current goal is HxY.
Let x be given.
Assume Hx: x ∈ (X ∖ V) ∩ Y.
We prove the intermediate claim HxXV: x ∈ X ∖ V.
An exact proof term for the current goal is (binintersectE1 (X ∖ V) Y x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 (X ∖ V) Y x Hx).
We prove the intermediate claim HxnotV: 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 HxY.
Assume HxVY: x ∈ V ∩ Y.
Apply HxnotV to the current goal.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
We use C to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HCclosed.
An exact proof term for the current goal is HAeqC.
Assume Hexists: ∃C : set, closed_in X Tx C ∧ A = C ∩ Y.
We will prove closed_in Y (subspace_topology X Tx Y) A.
Apply Hexists to the current goal.
Let C be given.
Assume HCandEq.
Apply HCandEq to the current goal.
Assume HCclosed: closed_in X Tx C.
Assume HAeq: A = C ∩ Y.
We prove the intermediate claim HTsubspace: topology_on Y (subspace_topology X Tx Y).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HY).
We prove the intermediate claim HCdef: topology_on X Tx ∧ (C ⊆ X ∧ ∃V ∈ Tx, C = X ∖ V).
An exact proof term for the current goal is HCclosed.
We prove the intermediate claim HCandEx: C ⊆ X ∧ ∃V ∈ Tx, C = X ∖ V.
An exact proof term for the current goal is (andER (topology_on X Tx) (C ⊆ X ∧ ∃V ∈ Tx, C = X ∖ V) HCdef).
We prove the intermediate claim HexV: ∃V ∈ Tx, C = X ∖ V.
An exact proof term for the current goal is (andER (C ⊆ X) (∃V ∈ Tx, C = X ∖ V) HCandEx).
Apply HexV to the current goal.
Let V be given.
Assume HVandEq.
Apply HVandEq to the current goal.
Assume HV: V ∈ Tx.
Assume HCeq: C = X ∖ V.
Set U to be the term V ∩ Y.
We prove the intermediate claim HUsubspace: U ∈ subspace_topology X Tx Y.
We prove the intermediate claim HUinPowerY: U ∈ 𝒫 Y.
Apply PowerI to the current goal.
An exact proof term for the current goal is (binintersect_Subq_2 V Y).
We prove the intermediate claim HPred: ∃W ∈ Tx, U = W ∩ Y.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HV.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ Y) U HUinPowerY HPred).
We prove the intermediate claim HAeqYU: A = Y ∖ U.
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using HCeq (from left to right).
We will prove (X ∖ V) ∩ Y = Y ∖ (V ∩ Y).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ (X ∖ V) ∩ Y.
We prove the intermediate claim HxXV: x ∈ X ∖ V.
An exact proof term for the current goal is (binintersectE1 (X ∖ V) Y x Hx).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (binintersectE2 (X ∖ V) Y x Hx).
We prove the intermediate claim HxnotV: 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 HxY.
Assume HxVY: x ∈ V ∩ Y.
Apply HxnotV to the current goal.
An exact proof term for the current goal is (binintersectE1 V Y x HxVY).
Let x be given.
Assume Hx: x ∈ Y ∖ (V ∩ Y).
We prove the intermediate claim HxY: x ∈ Y.
An exact proof term for the current goal is (setminusE1 Y (V ∩ Y) x Hx).
We prove the intermediate claim HxnotVY: x ∉ V ∩ Y.
An exact proof term for the current goal is (setminusE2 Y (V ∩ Y) x Hx).
We prove the intermediate claim HxnotV: x ∉ V.
Assume HxV: x ∈ V.
Apply HxnotVY to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is HxV.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HY x HxY).
Apply binintersectI to the current goal.
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 HxnotV.
An exact proof term for the current goal is HxY.
We prove the intermediate claim HAsub: A ⊆ Y.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is (binintersect_Subq_2 C Y).
We will prove topology_on Y (subspace_topology X Tx Y) ∧ (A ⊆ Y ∧ ∃U ∈ subspace_topology X Tx Y, A = Y ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is HTsubspace.
Apply andI to the current goal.
An exact proof term for the current goal is HAsub.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUsubspace.
An exact proof term for the current goal is HAeqYU.
∎