Let X, Tx, Y and U be given.
Assume HTx: topology_on X Tx.
Assume HY: Y ⊆ X.
Assume HU: U ⊆ Y.
We will prove open_in Y (subspace_topology X Tx Y) U ↔ ∃V ∈ Tx, U = V ∩ Y.
Apply iffI to the current goal.
Assume HopenU: open_in Y (subspace_topology X Tx Y) U.
We will prove ∃V ∈ Tx, U = V ∩ Y.
We prove the intermediate claim HUinSubspace: U ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (andER (topology_on Y (subspace_topology X Tx Y)) (U ∈ subspace_topology X Tx Y) HopenU).
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HUinSubspace).
Assume Hexists: ∃V ∈ Tx, U = V ∩ Y.
We will prove open_in Y (subspace_topology X Tx Y) U.
We will prove topology_on Y (subspace_topology X Tx Y) ∧ U ∈ subspace_topology X Tx Y.
Apply andI to the current goal.
We will prove 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 will prove U ∈ subspace_topology X Tx Y.
Apply Hexists to the current goal.
Let V be given.
Assume HVpair: V ∈ Tx ∧ U = V ∩ Y.
We prove the intermediate claim HV: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U = V ∩ Y) HVpair).
We prove the intermediate claim HUeq: U = V ∩ Y.
An exact proof term for the current goal is (andER (V ∈ Tx) (U = V ∩ Y) HVpair).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V HV).
∎