norm_mul_le_max — Mathlib

English

In an ultrametric normed group, the norm satisfies ‖xy‖ ≤ max(‖x‖, ‖y‖).

Русский

В ультраметрической нормированной группе норма удовлетворяет ∥xy∥ ≤ max(∥x∥, ∥y∥).

LaTeX

$$$\\|xy\\| \\le \\max \\{\\|x\\|, \\|y\\|\\}$$$

Lean4

@[to_additive]
theorem norm_mul_le_max (x y : S) : ‖x * y‖ ≤ max ‖x‖ ‖y‖ := by
  simpa only [le_max_iff, dist_eq_norm_div, div_inv_eq_mul, div_one, one_mul] using dist_triangle_max x 1 y⁻¹

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