uniformOfFinset_apply

Mathlib.Probability.Distributions.Uniform

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

English

There exists a density for X with respect to μ and ℙ; i.e., HasPDF X ℙ μ.

Русский

Существует плотность для X относительно μ и ℙ; то есть HasPDF X ℙ μ.

LaTeX

$$$\\text{HasPDF}(X,\\mathbb{P},\\mu)$$$

Lean4

@[simp]
theorem uniformOfFinset_apply (a : α) : uniformOfFinset s hs a = if a ∈ s then (s.card : ℝ≥0∞)⁻¹ else 0 :=
  rfl

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

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

Разделы

Аффилиация

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