indepSets

Mathlib.Probability.Independence.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Indep.indepSets

← MathLib Explorer

English

If Indep (generateFrom s1) (generateFrom s2) μ holds, then IndepSets s1 s2 μ.

Русский

Если Indep(generateFrom s1, generateFrom s2; μ) держится, то IndepSets s1 s2 μ.

LaTeX

$$Indep(generateFrom s1, generateFrom s2; μ) ⇒ IndepSets s1 s2 μ$$

Lean4

theorem indepSets {s1 s2 : Set (Set Ω)} (h_indep : Indep (generateFrom s1) (generateFrom s2) μ) : IndepSets s1 s2 μ :=
  Kernel.Indep.indepSets h_indep

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

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

Разделы

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

Аффилиация

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