norm_div_eq_max_of_norm_div_ne_norm_div

English

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

Русский

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

LaTeX

$$$\\|x/y\\| ≠ \\|y/z\\| \\Rightarrow \\|x/z\\| = \\max\\left(\\|x/y\\|, \\|y/z\\|\\right)$$$

Lean4

/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive /-- All triangles are isosceles in an ultrametric normed additive group. -/
    ]
theorem norm_div_eq_max_of_norm_div_ne_norm_div (x y z : S) (h : ‖x / y‖ ≠ ‖y / z‖) : ‖x / z‖ = max ‖x / y‖ ‖y / z‖ :=
  by simpa only [div_mul_div_cancel] using norm_mul_eq_max_of_norm_ne_norm h

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