isClosedEmbedding_coe_real — Mathlib

English

The inclusion ℕ → ℝ is a closed embedding; i.e., the image of a closed set is closed in ℝ and the embedding is a topological embedding with closed image.

Русский

Включение ℕ в ℝ является замкнутым вложением; образ замкнутого множества является замкнутым в ℝ, и это встраивание сохраняет топологию.

LaTeX

$$$\operatorname{IsClosedEmbedding}(\operatorname{Nat.cast})$$$

Lean4

theorem isClosedEmbedding_coe_real : IsClosedEmbedding ((↑) : ℕ → ℝ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

Похожие утверждения