Let X, Tx, Fam and Y be given.
Assume HFam: open_cover_of X Tx Fam.
Assume HYsub: Y ⊆ X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (open_cover_of_topology X Tx Fam HFam).
We prove the intermediate claim HTy: 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 HYsub).
We prove the intermediate claim HsubPow: restrict_family_to_subspace Fam Y ⊆ 𝒫 Y.
An exact proof term for the current goal is (restrict_family_to_subspace_subset_Power Fam Y).
We prove the intermediate claim HYcov: Y ⊆ ⋃ (restrict_family_to_subspace Fam Y).
Let y be given.
Assume HyY: y ∈ Y.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim HyUnionFam: y ∈ ⋃ Fam.
An exact proof term for the current goal is (open_cover_of_covers X Tx Fam HFam y HyX).
Apply (UnionE Fam y HyUnionFam) to the current goal.
Let U be given.
Assume Hypair: y ∈ U ∧ U ∈ Fam.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (andEL (y ∈ U) (U ∈ Fam) Hypair).
We prove the intermediate claim HUfam: U ∈ Fam.
An exact proof term for the current goal is (andER (y ∈ U) (U ∈ Fam) Hypair).
We prove the intermediate claim HyUy: y ∈ U ∩ Y.
An exact proof term for the current goal is (binintersectI U Y y HyU HyY).
We prove the intermediate claim HUres: U ∩ Y ∈ restrict_family_to_subspace Fam Y.
An exact proof term for the current goal is (ReplI Fam (λU0 : set ⇒ U0 ∩ Y) U HUfam).
An exact proof term for the current goal is (UnionI (restrict_family_to_subspace Fam Y) y (U ∩ Y) HyUy HUres).
We prove the intermediate claim HmemOpen: ∀U : set, U ∈ restrict_family_to_subspace Fam Y → U ∈ subspace_topology X Tx Y.
Let W be given.
Assume HW: W ∈ restrict_family_to_subspace Fam Y.
Apply (ReplE_impred Fam (λU : set ⇒ U ∩ Y) W HW (W ∈ subspace_topology X Tx Y)) to the current goal.
Let U be given.
Assume HUfam: U ∈ Fam.
Assume HWeq: W = U ∩ Y.
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (open_cover_of_members_open X Tx Fam U HFam HUfam).
We prove the intermediate claim HWin: (U ∩ Y) ∈ subspace_topology X Tx Y.
An exact proof term for the current goal is (subspace_topologyI X Tx Y U HUopen).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HWin.
Apply (open_cover_ofI Y (subspace_topology X Tx Y) (restrict_family_to_subspace Fam Y)) to the current goal.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is HsubPow.
An exact proof term for the current goal is HYcov.
An exact proof term for the current goal is HmemOpen.
∎