support_normalize — Mathlib

English

Let f: α → ℝ≥0∞ with tsum f ≠ 0 and tsum f ≠ ∞. Then the support of the normalized f equals the support of f.

Русский

Пусть f: α → ℝ≥0∞ такa, что сумма tsum f не равна нулю и не бесконечна. Тогда опорa нормализованного f равна опоре f.

LaTeX

$$$\\operatorname{supp}(\\operatorname{normalize} f\\; hf0\\; hf) = \\operatorname{supp}(f)$$$

Lean4

@[simp]
theorem support_normalize : (normalize f hf0 hf).support = Function.support f :=
  Set.ext fun a => by simp [hf, mem_support_iff]

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