mem_support_ofFinset_iff

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

English

For a ∈ α, a belongs to the support of ofFinset f s h h' iff a ∈ s and f(a) ≠ 0.

Русский

Для a принадлежит опоре ofFinset f s h h' тогда и только тогда, когда a ∈ s и f(a) ≠ 0.

LaTeX

$$$ a \in (ofFinset f s h h').support \iff a \in s \land f a \neq 0 $$$

Lean4

theorem mem_support_ofFinset_iff (a : α) : a ∈ (ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0 := by simp

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

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

Разделы

Аффилиация

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