measurable_countablePartitionSet — Mathlib

English

For countableFiltration, the function countablePartitionSet n is measurable.

Русский

Для countableFiltration функция countablePartitionSet n измерима.

LaTeX

$$$$ \Measurable (countablePartitionSet n) $$$$

Lean4

theorem measurable_countablePartitionSet (α : Type*) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
    Measurable (countablePartitionSet (α := α) n) :=
  (measurable_countableFiltration_countablePartitionSet α n).mono ((countableFiltration α).le n) le_rfl

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