support_uniformOfFinset

Mathlib.Probability.Distributions.Uniform

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

← MathLib Explorer

English

UniformPDF s x μ is the density that equals (μ(s))⁻¹ if x ∈ s and 0 otherwise.

Русский

UniformPDF s x μ равно (μ(s))⁻¹ при x∈s и равно 0 иначе.

LaTeX

$$$\\text{uniformPDF}(s,x,\\mu)=\\begin{cases}(\\mu(s))^{-1} & x\\in s, \\\\ 0 & \\text{else}.\\end{cases}$$$

Lean4

@[simp]
theorem support_uniformOfFinset : (uniformOfFinset s hs).support = s :=
  Set.ext
    (by
      let ⟨a, ha⟩ := hs
      simp [mem_support_iff])

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

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

Разделы

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

Аффилиация

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