mem_support_map_iff

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

English

Another equivalent formulation of the support description for the mapped PMF.

Русский

Ещё одно эквивалентное описание опоры для отображённой PMF.

LaTeX

$$$ b \\in (map f p).\\mathrm{support} \\iff \\exists a, a \\in p.\\mathrm{support} \\land f(a) = b$$$

Lean4

theorem mem_support_map_iff : b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b := by simp

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

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

Разделы

Аффилиация

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