generateFrom_countablePartition_le

English

For α with a countably generated measurable space, the sigma-algebra generated by countablePartition α n is contained in the ambient measurable space m: generateFrom (countablePartition α n) ≤ m.

Русский

Для α с счетно генерируемым пространством измеримости сигма-алгебра, порождаемая countablePartition α n, содержится в m: generateFrom(countablePartition α n) ≤ m.

LaTeX

$$$$ \\operatorname{generateFrom}(\\text{countablePartition }\\alpha n) \\le m. $$$$

Lean4

theorem generateFrom_countablePartition_le (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
    generateFrom (countablePartition α n) ≤ m :=
  generateFrom_memPartition_le (measurableSet_enumerateCountable_countableGeneratingSet α) n

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