sub

Mathlib.Analysis.Normed.Lp.lpSpace

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

English

If f ∈ ℓ^p, then c • f ∈ ℓ^p for any scalar c (from a normed ring).

Русский

Если f ∈ ℓ^p, то для любого скаляра c выполнено c • f ∈ ℓ^p.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(f,p) \Rightarrow \mathrm{Mem}_{\ell^p}(c \cdot f,p). $$$$

Lean4

theorem sub {f g : ∀ i, E i} (hf : Memℓp f p) (hg : Memℓp g p) : Memℓp (f - g) p := by rw [sub_eq_add_neg];
  exact hf.add hg.neg

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

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

Разделы

Аффилиация

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