indepSets_zero_left

Mathlib.Probability.Independence.Kernel

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.indepSets_zero_left

English

Similarly, iIndepSets s1 s2 0 μ holds for any μ.

Русский

Аналогично, iIndepSets s1 s2 0 μ выполняется для любого μ.

LaTeX

$$$iIndepSets\, s_1\, s_2\, 0\, μ$$$

Lean4

@[simp]
theorem indepSets_zero_left : IndepSets s1 s2 (0 : Kernel α Ω) μ := by simp [IndepSets]

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

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

Разделы

Аффилиация

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