filter_apply_ne_zero_iff

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

← MathLib Explorer

English

(p.filter s h) a ≠ 0 iff a ∈ s ∧ a ∈ p.support.

Русский

(p.filter s h) a ≠ 0 эквивалентно a ∈ s ∧ a ∈ поддержке p.

LaTeX

$$$ (p.filter\ s\ h)(a) \neq 0 \iff a \in s \land a \in p.\mathrm{support} $$$

Lean4

theorem filter_apply_ne_zero_iff (a : α) : (p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support := by
  rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]

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

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

Разделы

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

Аффилиация

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