nndist_nnnorm_nnnorm_le' — Mathlib

English

For a,b in E, the NN-norm distance between ‖a‖₊ and ‖b‖₊ is bounded above by ‖a/b‖₊: nndist ‖a‖₊ ‖b‖₊ ≤ ‖a/b‖₊.

Русский

Для любых a,b: nndist(‖a‖₊,‖b‖₊) ≤ ‖a/b‖₊.

LaTeX

$$$$ \\operatorname{nndist}( \\|a\\|_{+}, \\|b\\|_{+} ) \\leq \\|a / b\\|_{+} $$$$

Lean4

@[to_additive nndist_nnnorm_nnnorm_le]
theorem nndist_nnnorm_nnnorm_le' (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊ :=
  NNReal.coe_le_coe.1 <| dist_norm_norm_le' a b

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