generateFrom_iUnion_memPartition_le

English

If every t(n) is measurable, then generateFrom (⋃ n memPartition t n) ≤ m.

Русский

Если каждый t(n) измерим, то generateFrom(⋃n memPartition t n) ≤ m.

LaTeX

$$$ generateFrom(\bigcup_{n} memPartition(t,n)) \leq m $$$

Lean4

theorem generateFrom_iUnion_memPartition_le [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ n, MeasurableSet (t n)) :
    generateFrom (⋃ n, memPartition t n) ≤ m :=
  by
  refine (generateFrom_iUnion_memPartition t).trans_le (generateFrom_le ?_)
  rintro s ⟨i, rfl⟩
  exact ht i

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