isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one

English

Let R be a normed division ring. If for all x ∈ R, ∥x∥ ≤ 1 implies ∥x-1∥ ≤ 1, then IsUltrametricDist R.

Русский

Пусть R — нормированное делимое кольцо. Если для всех x ∈ R с ∥x∥ ≤ 1 выполняется ∥x-1∥ ≤ 1, то IsUltrametricDist R.

LaTeX

$$$\\forall x\\in R, \\|x\\| \\le 1 \\Rightarrow \\|x-1\\| \\le 1 \\Longrightarrow \\mathrm{IsUltrametricDist}(R)$$$

Lean4

theorem isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one (h : ∀ x : R, ‖x‖ ≤ 1 → ‖x - 1‖ ≤ 1) :
    IsUltrametricDist R :=
  by
  have (x : R) (hx : ‖x‖ ≤ 1) : ‖x + 1‖ ≤ 1 := by simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)
  exact isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

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