nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div

English

Similarly for nnnorm: if ‖(x/y)‖₊ ≠ ‖(y/z)‖₊ then ‖(x/z)‖₊ = max(‖(x/y)‖₊, ‖(y/z)‖₊).

Русский

Аналогично для nnnorm: если ‖x/y‖₊ ≠ ‖y/z‖₊, то ‖x/z‖₊ = max(‖x/y‖₊, ‖y/z‖₊).

LaTeX

$$$\\|x/y\\|_{+} ≠ \\|y/z\\|_{+} \\Rightarrow \\|x/z\\|_{+} = \\max(\\|x/y\\|_{+}, \\|y/z\\|_{+})$$$

Lean4

/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive /-- All triangles are isosceles in an ultrametric normed additive group. -/
    ]
theorem nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div (x y z : S) (h : ‖x / y‖₊ ≠ ‖y / z‖₊) :
    ‖x / z‖₊ = max ‖x / y‖₊ ‖y / z‖₊ := by
  simpa only [← NNReal.coe_inj, NNReal.coe_max] using
    norm_div_eq_max_of_norm_div_ne_norm_div _ _ _ (NNReal.coe_injective.ne h)

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