English
If α is finite, then every f: ∀ i, E_i belongs to ℓ^p with p ∈ [0, ∞]; i.e., Memℓp f p holds for any such f.
Русский
Если индексный множество α конечно, то любой функтор f: α → E_i принадлежит ℓ^p для любого p, т.е. Memℓp f p выполняется.
LaTeX
$$$f \in \ell^p(E) \quad(\text{with } \alpha \text{ finite})$$$
Lean4
/-- When `α` is `Finite`, every `f : PreLp E p` satisfies `Memℓp f p`. -/
theorem all (f : ∀ i, E i) : Memℓp f p :=
by
rcases p.trichotomy with (rfl | rfl | _h)
· exact memℓp_zero_iff.mpr {i : α | f i ≠ 0}.toFinite
· exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)
· cases nonempty_fintype α; exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
