indep_bot_right — Mathlib

English

Independence with a zero or probability measure on the right-hand side holds for the bottom sigma-algebra.

Русский

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

LaTeX

$$$\text{indep\_bot\_right}(m') : \text{Indep } m' \; \bot \; μ$$$

Lean4

theorem indep_bot_right [IsZeroOrProbabilityMeasure μ] : Indep m' ⊥ μ :=
  Kernel.indep_bot_right m'

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