measurableSet_succ_memPartition — Mathlib

English

If s ∈ memPartition t n, then s is measurable in generateFrom (memPartition t (n+1)).

Русский

Если s ∈ memPartition t n, то s измеримо относительно generateFrom (memPartition t (n+1)).

LaTeX

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

Lean4

theorem measurableSet_succ_memPartition (t : ℕ → Set α) (n : ℕ) {s : Set α} (hs : s ∈ memPartition t n) :
    MeasurableSet[generateFrom (memPartition t (n + 1))] s :=
  by
  rw [← diff_union_inter s (t n)]
  refine MeasurableSet.union ?_ ?_ <;>
    · refine measurableSet_generateFrom ?_
      rw [memPartition_succ]
      exact ⟨s, hs, by simp⟩

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