ofMultiset_apply_of_notMem — Mathlib

English

If an element a does not occur in s, then the PMF value at a is zero.

Русский

Если элемент a не встречается в s, то значение PMF в точке a равно нулю.

LaTeX

$$$$ \\mathrm{ofMultiset\\_apply\\_of\\_notMem}\\; (hs)\\; (a) = 0 $$$$

Lean4

theorem ofMultiset_apply_of_notMem {a : α} (ha : a ∉ s) : ofMultiset s hs a = 0 := by
  simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero,
    ENNReal.natCast_ne_top, or_false] using ha

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