uniformOn_inter'

Mathlib.Probability.UniformOn

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.uniformOn_inter'

← MathLib Explorer

English

For finite s, uniformOn s (t ∩ u) = uniformOn (s ∩ u) t · uniformOn s u.

Русский

Для конечного s: uniformOn s (t ∩ u) = uniformOn (s ∩ u) t · uniformOn s u.

LaTeX

$$$uniformOn\\; s\\; (t \\cap u) = uniformOn\\; (s \\cap u)\\; t \\cdot uniformOn\\; s\\; u$$$

Lean4

theorem uniformOn_inter' (hs : s.Finite) : uniformOn s (t ∩ u) = uniformOn (s ∩ u) t * uniformOn s u :=
  by
  rw [← Set.inter_comm]
  exact uniformOn_inter hs

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

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

Разделы

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

Аффилиация

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