norm_eq_card_dsupport — Mathlib

English

For f in lp E 0, the norm equals the cardinality of its finite support.

Русский

Для f ∈ lp E 0 нормa равна мощности множества индексов, на которых f не равен нулю (сколько ненулевых координат).

LaTeX

$$$\\|f\\| = \\#\\operatorname{supp}_{\\text{finite}}(f) = (lp.memℓp f).finite_dsupport.toFinset.card$$$

Lean4

theorem norm_eq_card_dsupport (f : lp E 0) : ‖f‖ = (lp.memℓp f).finite_dsupport.toFinset.card :=
  dif_pos rfl

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