indep_of_indep_of_le_left — Mathlib

English

If two sigma-algebras m1 and m2 are independent with respect to a kernel κ and a measure μ, then any coarser left sigma-algebra m3 ⊆ m1 is also independent from m2 with respect to κ and μ.

Русский

Если две сигма-алгебры m1 и m2 независимы относительно ядерной распределения κ и меры μ, то любая более грубая левая сигма-алгебра m3 ⊆ m1 также независима от m2 по отношению к κ и μ.

LaTeX

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

Lean4

theorem indep_of_indep_of_le_left {m₁ m₂ m₃ : MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω}
    {μ : Measure α} (h_indep : Indep m₁ m₂ κ μ) (h31 : m₃ ≤ m₁) : Indep m₃ m₂ κ μ := fun t1 t2 ht1 ht2 =>
  h_indep t1 t2 (h31 _ ht1) ht2

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