nnnorm_eq_of_mul_nnnorm_lt_max — Mathlib

English

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

Русский

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

LaTeX

$$$\\|xy\\|_{+} < \\max(\\|x\\|_{+}, \\|y\\|_{+}) \\Rightarrow \\|x\\|_{+} = \\|y\\|_{+}$$$

Lean4

@[to_additive]
theorem nnnorm_eq_of_mul_nnnorm_lt_max {x y : S} (h : ‖x * y‖₊ < max ‖x‖₊ ‖y‖₊) : ‖x‖₊ = ‖y‖₊ :=
  not_ne_iff.mp (h.ne ∘ nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm)

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