indepSet_of_mem — Mathlib

English

If s ∈ S and t ∈ T with S, T families of sets, and S, T are measurable, and the big independence hypothesis holds, then IndepSet s t κ μ.

Русский

Если s принадлежит S, t принадлежит T, при условии измеримости и независимости, то IndepSet s t κ μ.

LaTeX

$$$IndepSets S T κ μ \Rightarrow IndepSet s t κ μ$$$

Lean4

theorem indepSet_of_mem {_m0 : MeasurableSpace Ω} (hs : s ∈ S) (ht : t ∈ T) (hs_meas : MeasurableSet s)
    (ht_meas : MeasurableSet t) (κ : Kernel α Ω) (μ : Measure α) [IsZeroOrMarkovKernel κ]
    (h_indep : IndepSets S T κ μ) : IndepSet s t κ μ :=
  (indepSet_iff_measure_inter_eq_mul hs_meas ht_meas κ μ).mpr (h_indep s t hs ht)

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