instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty

English

If the index class I is nonempty, then the space lp B ∞ has a NormOneClass structure, i.e., there exists an element of unit norm compatible with the subspace structure.

Русский

Если множество индексов непусто, тогда пространство lp B ∞ имеет структуру нормы единицы, т.е. существует элемент нулевой нормы равной единице в подпространстве.

LaTeX

$$$\text{NormOne}(lp B \infty) \text{ exists when } I \neq \varnothing.$$$

Lean4

instance [Nonempty I] : NormOneClass (lp B ∞) where
  norm_one := by simp_rw [lp.norm_eq_ciSup, infty_coeFn_one, Pi.one_apply, norm_one, ciSup_const]

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