enorm_inv'

Mathlib.Analysis.Normed.Group.Basic

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

English

For any a ∈ E, ‖a⁻¹‖ₑ = ‖a‖ₑ; the EN-norm is invariant under taking inverses.

Русский

Для любого a ∈ E: ‖a⁻¹‖ₑ = ‖a‖ₑ; норма инвариантна к взятию обратного.

LaTeX

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

Lean4

@[to_additive (attr := simp) enorm_neg]
theorem enorm_inv' (a : E) : ‖a⁻¹‖ₑ = ‖a‖ₑ := by simp [enorm]

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

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

Разделы

Аффилиация

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