indepSet_zero_left

Mathlib.Probability.Independence.Kernel

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

English

Similarly, IndepSet s t κ 0 μ holds.

Русский

Аналогично, IndepSet s t κ 0 μ выполняется.

LaTeX

$$$IndepSet\, s\, t\, κ\, 0\, μ$$$

Lean4

@[simp]
theorem indepSet_zero_left {s t : Set Ω} : IndepSet s t (0 : Kernel α Ω) μ := by simp [IndepSet]

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

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

Разделы

Аффилиация

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