neg — Mathlib

English

If f ∈ ℓ^p, then −f ∈ ℓ^p as well.

Русский

Если f ∈ ℓ^p, то −f также ∈ ℓ^p.

LaTeX

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

Lean4

theorem neg {f : ∀ i, E i} (hf : Memℓp f p) : Memℓp (-f) p :=
  by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    simp [hf.finite_dsupport]
  · apply memℓp_infty
    simpa using hf.bddAbove
  · apply memℓp_gen
    simpa using hf.summable hp

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