We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HtopPlane: topology_on EuclidPlane R2_standard_topology.
An exact proof term for the current goal is (product_topology_is_topology R R_standard_topology R R_standard_topology HtopR HtopR).
We prove the intermediate claim Hall: ∀U ∈ rectangular_regions, U ∈ R2_standard_topology.
Let U be given.
Assume HU: U ∈ rectangular_regions.
An exact proof term for the current goal is (rectangular_regions_subset_R2_standard_topology U HU).
An exact proof term for the current goal is (generated_topology_finer_weak EuclidPlane rectangular_regions R2_standard_topology HtopPlane Hall).
∎