ofFinset — Mathlib

English

Given a finite set s and a function f: α → ℝ≥0∞ with sum over s equal to 1, and zero outside s, one obtains a PMF on α.

Русский

Дано сконеченная множество s и функция f: α → ℝ≥0∞ с суммой по s равной 1 и нулевой вне s, тогда получаем PMF на α.

LaTeX

$$$ PMF.ofFinset f s h h' : PMF α $$$

Lean4

/-- Given a finset `s` and a function `f : α → ℝ≥0∞` with sum `1` on `s`,
  such that `f a = 0` for `a ∉ s`, we get a `PMF`. -/
def ofFinset (f : α → ℝ≥0∞) (s : Finset α) (h : ∑ a ∈ s, f a = 1) (h' : ∀ (a) (_ : a ∉ s), f a = 0) : PMF α :=
  ⟨f, h ▸ hasSum_sum_of_ne_finset_zero h'⟩

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