symm

Mathlib.Probability.Independence.Basic

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

English

Any independence relation persists when adding or removing a trivial (empty) or full sigma-algebra.

Русский

Любое отношение независимости сохраняется при добавлении или удалении тривиальной сигма-алгебры.

LaTeX

$$$\text{IndepSets}(s, μ) \Rightarrow \text{IndepSets}(s, μ)$$$

Lean4

@[symm]
theorem symm (h : Indep m₁ m₂ μ) : Indep m₂ m₁ μ :=
  IndepSets.symm h

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

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

Разделы

Аффилиация

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