isUltrametricDist_of_forall_norm_add_one_le_max_norm_one

English

Let R be a normed division ring. If for all x ∈ R we have ∥x+1∥ ≤ max(∥x∥, 1), then the distance on R is ultrametric.

Русский

Пусть R — нормированное делимое кольцо. Если для всякого элемента x выполняется ∥x+1∥ ≤ max(∥x∥, 1), то расстояние на R является ультраметрическим.

LaTeX

$$$\\forall x \\in R, \\|x+1\\| \\le \\max(\\|x\\|, 1) \\Longrightarrow \\text{IsUltrametricDist}(R)$$$

Lean4

theorem isUltrametricDist_of_forall_norm_add_one_le_max_norm_one (h : ∀ x : R, ‖x + 1‖ ≤ max ‖x‖ 1) :
    IsUltrametricDist R :=
  by
  refine isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)
  rcases eq_or_ne y 0 with rfl | hy
  · simpa only [add_zero] using le_max_left _ _
  · have p : 0 < ‖y‖ := norm_pos_iff.mpr hy
    simpa only [div_add_one hy, norm_div, div_le_iff₀ p, max_mul_of_nonneg _ _ p.le, one_mul,
      div_mul_cancel₀ _ p.ne'] using h (x / y)

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