Let X and N be given.
Assume HN: N ∈ ω.
Assume HX: X ⊆ (euclidean_space N).
Assume Hcomp: compact_space X (subspace_topology (euclidean_space N) (euclidean_topology N) X).
An exact proof term for the current goal is (compact_subspace_Rn_dimension_le N X HN HX Hcomp).
∎