zero_memℓp — Mathlib

English

The zero function belongs to every ℓp space for any p.

Русский

Нулевая функция принадлежит каждому ℓ^p пространства для любого p.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(0,p). $$$$

Lean4

theorem zero_memℓp : Memℓp (0 : ∀ i, E i) p :=
  by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    simp
  · apply memℓp_infty
    simp only [norm_zero, Pi.zero_apply]
    exact bddAbove_singleton.mono Set.range_const_subset
  · apply memℓp_gen
    simp [Real.zero_rpow hp.ne', summable_zero]

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