norm_mul_eq_max_of_norm_ne_norm — Mathlib

English

If ‖x‖ ≠ ‖y‖ then ‖xy‖ = max(‖x‖, ‖y‖).

Русский

Если ‖x‖ ≠ ‖y‖, то ‖xy‖ = max(‖x‖,‖y‖).

LaTeX

$$$\\|xy\\| = \\max(\\|x\\|, \\|y\\|)$ whenever $\\|x\\| \\neq \\|y\\|$$$

Lean4

/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive /-- All triangles are isosceles in an ultrametric normed additive group. -/
    ]
theorem norm_mul_eq_max_of_norm_ne_norm {x y : S} (h : ‖x‖ ≠ ‖y‖) : ‖x * y‖ = max ‖x‖ ‖y‖ :=
  by
  rw [← div_inv_eq_mul, ← dist_eq_norm_div, dist_eq_max_of_dist_ne_dist _ 1 _ (by simp [h])]
  simp only [dist_one_right, dist_one_left, norm_inv']

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