indepSet_empty_right

Mathlib.Probability.Independence.Kernel

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

← MathLib Explorer

English

Symmetric counterpart of indep_bot_right: Indep ⊥ m' κ μ.

Русский

Симметричный аналог indep_bot_right: Indep ⊥ m' κ μ.

LaTeX

$$$ Indep ⊥ m' κ μ = (indep\\_bot\\_right m').symm $$$

Lean4

theorem indepSet_empty_right {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ]
    (s : Set Ω) : IndepSet s ∅ κ μ :=
  by
  simp only [IndepSet, generateFrom_singleton_empty]
  exact indep_bot_right _

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

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

Разделы

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

Аффилиация

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