English
Let (s_i) be a family of measurable sets indexed by i in a preordered index set. If the family is independent in the sense of iIndepSet with respect to a kernel κ and a measure μ, then for any i and k with i < k, the sigma-algebra generated by s_k is independent of the sigma-algebra generated by all s_j with j ≤ i (with respect to κ and μ).
Русский
Пусть {s_i} — семейство измеримых множеств, индексированное по предопорядку, и пусть оно независимо в смысле iIndepSet относительно κ и μ. Тогда для любых i < k алгебра сигм, сгенерированная множеством s_k, независима от алгебры сигм, сгенерированной всеми s_j с j ≤ i (относительно κ и μ).
LaTeX
$$$Indep\left( \sigma(\{s_k\}), \sigma\left(\{t \mid \exists j \le i,\ s_j = t\}\right) \right)\ κ\ μ$$$
Lean4
theorem indep_generateFrom_le [Preorder ι] {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ)
(i : ι) {k : ι} (hk : i < k) : Indep (generateFrom {s k}) (generateFrom {t | ∃ j ≤ i, s j = t}) κ μ :=
by
convert
iIndepSet.indep_generateFrom_of_disjoint hsm hs { k } {j | j ≤ i} (Set.disjoint_singleton_left.mpr hk.not_ge) using
1
simp only [Set.mem_singleton_iff, exists_eq_left, Set.setOf_eq_eq_singleton']
