generateFrom_memPartition_le_succ

English

The generated sigma-algebras are monotone with respect to taking successors: generateFrom(memPartition t n) ≤ generateFrom(memPartition t (n+1)).

Русский

Порожденные сигма-алгебры возрастают при переходе к следующему элементу разбиения: generateFrom(memPartition t n) ≤ generateFrom(memPartition t (n+1)).

LaTeX

$$generateFrom (memPartition t n) ≤ generateFrom (memPartition t (n + 1))$$

Lean4

theorem generateFrom_memPartition_le_succ (t : ℕ → Set α) (n : ℕ) :
    generateFrom (memPartition t n) ≤ generateFrom (memPartition t (n + 1)) :=
  generateFrom_le (fun _ hs ↦ measurableSet_succ_memPartition t n hs)

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