Let N and X be given.

Assume HN: N ∈ ω.

Assume HXsub: X ⊆ (euclidean_space N).

Assume Hcomp: compact_space X (subspace_topology (euclidean_space N) (euclidean_topology N) X).

Set EN to be the term euclidean_space N.

Set TN to be the term euclidean_topology N.

Set Xi to be the term const_space_family N R R_standard_topology.

We prove the intermediate claim HHfam: Hausdorff_spaces_family N Xi.

Let i be given.

Assume Hi: i ∈ N.

We will prove Hausdorff_space (product_component Xi i) (product_component_topology Xi i).

rewrite the current goal using (product_component_def Xi i) (from left to right).

rewrite the current goal using (product_component_topology_def Xi i) (from left to right).

rewrite the current goal using (const_space_family_apply N 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 R_standard_topology_Hausdorff.

We prove the intermediate claim HH: Hausdorff_space EN TN.

An exact proof term for the current goal is (product_topology_full_Hausdorff_axiom N Xi HHfam).

We prove the intermediate claim HclX: closed_in EN TN X.

An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed EN TN X HH HXsub Hcomp).

We prove the intermediate claim HdimEN: covering_dimension EN TN N.

An exact proof term for the current goal is (euclidean_space_covering_dimension_le N HN).

An exact proof term for the current goal is (dimension_closed_subspace_le EN TN X N HdimEN HclX).

∎