ofFinset_apply

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

English

For a ∈ α, the value of ofFinset at a equals f(a).

Русский

Для любого a ∈ α значение ofFinset(a) равно f(a).

LaTeX

$$$ ofFinset f s h h' a = f a $$$

Lean4

@[simp]
theorem ofFinset_apply (a : α) : ofFinset f s h h' a = f a :=
  rfl

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

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

Разделы

Аффилиация

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