measurableSet_generateFrom_memPartition

English

For every n, the set t(n) is measurable with respect to the sigma-algebra generated by memPartition t (n+1).

Русский

Для каждого n множество t(n) измеримо относительно сигма-алгебры, порождаемой memPartition t (n+1).

LaTeX

$$$\MeasurableSet[generateFrom(memPartition\ t\ (n+1))](t\ n)$$$

Lean4

theorem measurableSet_generateFrom_memPartition (t : ℕ → Set α) (n : ℕ) :
    MeasurableSet[generateFrom (memPartition t (n + 1))] (t n) :=
  by
  have : t n = ⋃ u ∈ memPartition t n, u ∩ t n := by
    simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]
  rw [this]
  refine MeasurableSet.biUnion (finite_memPartition _ _).countable (fun v hv ↦ ?_)
  refine measurableSet_generateFrom ?_
  rw [memPartition_succ]
  exact ⟨v, hv, Or.inl rfl⟩

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