nnnorm_commutator_units_sub_one_le

English

In a normed ring, for units a,b, the NN-norm of the commutator deviation is bounded by the same product as above in NNReal terms.

Русский

В нормированном кольце для единиц a, b неотрицательная нормa коммутатора ограничена тем же произведением в терминах NNReal, что и ранее.

LaTeX

$$$\|a b a^{-1} b^{-1} - 1\|_{+} ≤ 2 \|a^{-1}\|_{+} \|b^{-1}\|_{+} \|a - 1\|_{+} \|b - 1\|_{+}$$$

Lean4

theorem nnnorm_commutator_units_sub_one_le (a b : αˣ) :
    ‖(a * b * a⁻¹ * b⁻¹).val - 1‖₊ ≤ 2 * ‖a⁻¹.val‖₊ * ‖b⁻¹.val‖₊ * ‖a.val - 1‖₊ * ‖b.val - 1‖₊ := by
  simpa using norm_commutator_units_sub_one_le a b

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