filter_apply_eq_zero_of_notMem

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

← MathLib Explorer

English

If a ∉ s, then (p.filter s h) a = 0.

Русский

Если a ∉ s, то (p.filter s h) a = 0.

LaTeX

$$$ a \notin s \Rightarrow (p.filter\ s\ h)(a) = 0 $$$

Lean4

theorem filter_apply_eq_zero_of_notMem {a : α} (ha : a ∉ s) : (p.filter s h) a = 0 := by
  rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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