uniformOn_of_univ

Mathlib.Probability.UniformOn

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.uniformOn_of_univ

English

As above, uniformOn s Set.univ = 1 when s is finite and nonempty.

Русский

Как выше, если s конечна и непустa, uniformOn s Set.univ = 1.

LaTeX

$$$uniformOn\\; s\\; Set.univ = 1$$$

Lean4

theorem uniformOn_of_univ (hs : s.Finite) (hs' : s.Nonempty) : uniformOn s Set.univ = 1 :=
  uniformOn_eq_one_of hs hs' s.subset_univ

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

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

Разделы

Аффилиация

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