Let n be given.
Assume HnO: n ∈ ω.
We will prove metrizable (euclidean_space n) (euclidean_topology n).
We prove the intermediate claim Hreg: regular_space (euclidean_space n) (euclidean_topology n).
An exact proof term for the current goal is (euclidean_space_regular n).
We prove the intermediate claim Hscc: second_countable_space (euclidean_space n) (euclidean_topology n).
An exact proof term for the current goal is (euclidean_spaces_second_countable n HnO).
An exact proof term for the current goal is (Urysohn_metrization_theorem (euclidean_space n) (euclidean_topology n) Hreg Hscc).
∎