neg_iff

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#Memℓp.neg_iff

English

For any f, Memℓp(-f) = Memℓp(f).

Русский

Для любого f выполняется Memℓp(-f) = Memℓp(f).

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(-f,p) \iff \mathrm{Mem}_{\ell^p}(f,p). $$$$

Lean4

@[simp]
theorem neg_iff {f : ∀ i, E i} : Memℓp (-f) p ↔ Memℓp f p :=
  ⟨fun h => neg_neg f ▸ h.neg, Memℓp.neg⟩

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

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

Разделы

Аффилиация

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