support_ofFintype

Mathlib.Probability.ProbabilityMassFunction.Constructions

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

English

The support of the PMF obtained from a finite type equals the support of f.

Русский

Опора PMF, полученного из конечного типа, равна опоре функции f.

LaTeX

$$$ (ofFintype f h).support = Function.support f $$$

Lean4

@[simp]
theorem support_ofFintype : (ofFintype f h).support = Function.support f :=
  rfl

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

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

Разделы

Аффилиация

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