mem_support_normalize_iff — Mathlib

English

Let f : α → ℝ≥0∞ be a mass function with tsum f ≠ 0 and tsum f ≠ ∞. Then a belongs to the support of the normalized mass function normalize f hf0 hf if and only if f(a) ≠ 0.

Русский

Пусть f : α → ℝ≥0∞ имеет суммарную массу, не равную нулю и не равную бесконечности. Тогда a принадлежит поддержке нормализованной массы normalize f hf0 hf тогда и только тогда, когда f(a) ≠ 0.

LaTeX

$$$ a \in \operatorname{supp}(\operatorname{normalize}(f, hf0, hf)) \iff f(a) \neq 0 $$$

Lean4

theorem mem_support_normalize_iff (a : α) : a ∈ (normalize f hf0 hf).support ↔ f a ≠ 0 := by simp

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