norm_mul_sub_norm_div_le_two_mul_min

English

For a in a commutative normed group, ‖u v‖ − ‖u / v‖ ≤ 2·min(‖u‖, ‖v‖).

Русский

Для коммутативной нормированной группы: ‖u v‖ − ‖u / v‖ ≤ 2·min(‖u‖, ‖v‖).

LaTeX

$$$$ \|u v\| - \|u / v\| \le 2 \min( \|u\|, \|v\| ). $$$$

Lean4

@[to_additive norm_add_sub_norm_sub_le_two_mul_min]
theorem norm_mul_sub_norm_div_le_two_mul_min {E : Type*} [SeminormedCommGroup E] (u v : E) :
    ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖ :=
  by
  rw [mul_min_of_nonneg _ _ (by positivity)]
  refine le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)
  rw [norm_div_rev, mul_comm]
  exact
    norm_mul_sub_norm_div_le_two_mul _
      _
        -- Higher priority to fire before `mem_sphere`.

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