indepSet_empty_left

Mathlib.Probability.Independence.Basic

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

English

Symmetry of independence between two families of sets.

Русский

Симметрия независимости между двумя семействами множеств.

LaTeX

$$$\text{IndepSets}(s_1,s_2, μ) \iff \text{IndepSets}(s_2,s_1, μ)$$$

Lean4

theorem indepSet_empty_left [IsZeroOrProbabilityMeasure μ] (s : Set Ω) : IndepSet ∅ s μ :=
  Kernel.indepSet_empty_left s

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

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

Разделы

Аффилиация

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