measurableSet_countableFiltration_countablePartitionSet

English

For any n, t, MeasurableSet[countableFiltration α n] (countablePartitionSet n t).

Русский

Для любого n и t множество countablePartitionSet n t измеримо в countableFiltration α n.

LaTeX

$$$$ \MeasurableSet[countableFiltration α n](countablePartitionSet n t) $$$$

Lean4

theorem measurableSet_countableFiltration_countablePartitionSet (n : ℕ) (t : α) :
    MeasurableSet[countableFiltration α n] (countablePartitionSet n t) :=
  measurableSet_countableFiltration_of_mem n (countablePartitionSet_mem n t)

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