isUniformEmbedding_coe_real — Mathlib

English

The natural inclusion ℕ → ℝ is a uniform embedding; the map n ↦ n preserves uniform structure of the metric.

Русский

Естественное включение ℕ в ℝ является равномерным вложением; отображение n ↦ n сохраняет равномерную структуру метрики.

LaTeX

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

Lean4

theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℕ → ℝ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist

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