isUltrametricDist_iff_forall_norm_natCast_le_one

English

For NormedDivisionRing R, IsUltrametricDist R holds iff ∀ n ∈ ℕ, ∥(n : R)∥ ≤ 1.

Русский

Для нормированного делимого кольца R: IsUltrametricDist R эквивалентно тому, что ∀ n ∈ ℕ, ∥(n : R)∥ ≤ 1.

LaTeX

$$$\\mathrm{IsUltrametricDist}(R) \\iff \\forall n \\in \\mathbb{N}, \\|n\\| \\le 1$$$

Lean4

theorem isUltrametricDist_iff_forall_norm_natCast_le_one {R : Type*} [NormedDivisionRing R] :
    IsUltrametricDist R ↔ ∀ n : ℕ, ‖(n : R)‖ ≤ 1 :=
  ⟨fun _ => IsUltrametricDist.norm_natCast_le_one R, IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one⟩

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