generateFrom_memPartition_le_range

English

The sigma-algebra generated by memPartition t n is contained in the sigma-algebra generated by range t.

Русский

Сигма-алгебра, порождаемая memPartition t n, содержится в сигма-алгебре, порождаемой range t.

LaTeX

$$$generateFrom(memPartition(t,n)) \leq generateFrom(\operatorname{range}(t)).$$$

Lean4

theorem generateFrom_memPartition_le_range (t : ℕ → Set α) (n : ℕ) :
    generateFrom (memPartition t n) ≤ generateFrom (range t) :=
  by
  conv_rhs => rw [← generateFrom_iUnion_memPartition t]
  exact generateFrom_mono (subset_iUnion _ _)

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