ofFinset_apply_of_notMem

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.ofFinset_apply_of_notMem

English

If a is not in s, then the value of ofFinset at a is 0.

Русский

Если a не принадлежит s, то значение ofFinset(a) равно 0.

LaTeX

$$$ ofFinset f s h h' a = 0 \quad\text{(при } a \notin s) $$$

Lean4

theorem ofFinset_apply_of_notMem {a : α} (ha : a ∉ s) : ofFinset f s h h' a = 0 :=
  h' a ha

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru