enorm_inv

Mathlib.Analysis.Normed.Field.Basic

URI: https://scilib.ai/kg/mathlib#enorm_inv

English

For nonzero a, the ENNReal norm of the inverse is the reciprocal ENNReal norm: ||a^{-1}||_e = ||a||_e^{-1}.

Русский

При a ≠ 0 норма ENNReal обратного элемента равна обратной нормы ENNReal: ||a^{-1}||_e = ||a||_e^{-1}.

LaTeX

$$$\\|a^{-1}\\|_{e} = \\|a\\|_{e}^{-1}$$$

Lean4

@[simp]
theorem enorm_inv {a : α} (ha : a ≠ 0) : ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹ := by simp [enorm, ENNReal.coe_inv, ha]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru