indep_of_indep_of_le_right — Mathlib

English

Let m1, m2, m3 be sigma-algebras on Ω and μ a measure. If m3 ≤ m2 and m1 is independent of m2 with respect to μ, then m1 is independent of m3 with respect to μ.

Русский

Пусть Ω – множество, m1, m2, m3 – сигма-алгебры на Ω, μ – мера. Если m3 ⊆ m2 и m1 независима от m2 относительно μ, тогда m1 независима от m3 относительно μ.

LaTeX

$$$Indep(m_1, m_2; \\mu) \\land m_3 \\le m_2 \\Rightarrow Indep(m_1, m_3; \\mu)$$$

Lean4

theorem indep_of_indep_of_le_right (h_indep : Indep m₁ m₂ μ) (h32 : m₃ ≤ m₂) : Indep m₁ m₃ μ :=
  Kernel.indep_of_indep_of_le_right h_indep h32

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