Let m be given.
We will prove regular_space (euclidean_space m) (euclidean_topology m).
We prove the intermediate claim HRtop: 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 HregStd: regular_space R R_standard_topology.
An exact proof term for the current goal is (completely_regular_space_implies_regular R R_standard_topology R_standard_topology_completely_regular).
We prove the intermediate claim Hall: (∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi)) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi)).
An exact proof term for the current goal is (separation_axioms_subspace_product R R_standard_topology HRtop).
We prove the intermediate claim H123: ((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y)).
An exact proof term for the current goal is (andEL (((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y))) (∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi)) Hall).
We prove the intermediate claim H4: ∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi).
An exact proof term for the current goal is (andER (((∀Y : set, Y ⊆ R → Hausdorff_space R R_standard_topology → Hausdorff_space Y (subspace_topology R R_standard_topology Y)) ∧ (∀I Xi : set, Hausdorff_spaces_family I Xi → Hausdorff_space (product_space I Xi) (product_topology_full I Xi))) ∧ (∀Y : set, Y ⊆ R → regular_space R R_standard_topology → regular_space Y (subspace_topology R R_standard_topology Y))) (∀I Xi : set, regular_spaces_family I Xi → regular_space (product_space I Xi) (product_topology_full I Xi)) Hall).
We prove the intermediate claim Hfam: regular_spaces_family m (const_space_family m R R_standard_topology).
Let i be given.
Assume Hi: i ∈ m.
We will prove regular_space (product_component (const_space_family m R R_standard_topology) i) (product_component_topology (const_space_family m R R_standard_topology) i).
rewrite the current goal using (product_component_def (const_space_family m R R_standard_topology) i) (from left to right).
rewrite the current goal using (product_component_topology_def (const_space_family m R R_standard_topology) i) (from left to right).
rewrite the current goal using (const_space_family_apply m R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
An exact proof term for the current goal is HregStd.
An exact proof term for the current goal is (H4 m (const_space_family m R R_standard_topology) Hfam).
∎