isUltrametricDist_of_forall_norm_add_one_of_norm_le_one

English

Let R be a normed division ring. If for all x with ∥x∥ ≤ 1 we have ∥x+1∥ ≤ 1, then IsUltrametricDist R.

Русский

Пусть R — нормированное делимое кольцо. Если для всех x с ∥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_add_one_of_norm_le_one (h : ∀ x : R, ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1) :
    IsUltrametricDist R :=
  by
  refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_
  rcases le_or_gt ‖x‖ 1 with H | H
  · exact (h _ H).trans (le_max_right _ _)
  · suffices ‖x + 1‖ ≤ ‖x‖ from this.trans (le_max_left _ _)
    rw [← div_le_one (by positivity), ← norm_div, add_div, div_self (by simpa using H.trans' zero_lt_one), add_comm]
    apply h
    simp [inv_le_one_iff₀, H.le]

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