instMetricSpace — Mathlib

English

There exists a metric space structure on ℕ such that the inclusion into ℝ is an isometric embedding; equivalently, the metric on ℕ is the pullback of the real metric via Nat.cast.

Русский

Существует метрика на ℕ такая, что включение в ℝ является изометрическим вложением; метрика ℕ — это прообраз метрического пространства ℝ через Nat.cast.

LaTeX

$$$\operatorname{MetricSpace} \mathbb{N}$ with metric pulled back from \mathbb{R}$ via Nat.cast$$

Lean4

instance : MetricSpace ℕ :=
  Nat.isUniformEmbedding_coe_real.comapMetricSpace _

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