nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm

English

If Ne (nnnorm) is used with a product, then the product norm equals the max of the factors under a non-equality condition as above.

Русский

Если применяется nnnorm с произведением, то норма произведения равна максимуму норм при условии неравенства, как выше.

LaTeX

$$$\\text{nnnorm}(xy) = \\max(\\text{nnnorm}(x), \\text{nnnorm}(y))$ при неравенстве норм, как выше$$

Lean4

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

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