mem_support_uniformOfFinset_iff

Mathlib.Probability.Distributions.Uniform

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

English

uniformOfFinset has explicit support: its support equals the generating finite set.

Русский

uniformOfFinset имеет явную опору: её поддержка равна заданному конечному множеству.

LaTeX

$$$\\text{support}(\\text{uniformOfFinset}(s,\\, hs))=s$$$

Lean4

theorem mem_support_uniformOfFinset_iff (a : α) : a ∈ (uniformOfFinset s hs).support ↔ a ∈ s := by simp

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

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

Разделы

Аффилиация

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