measurable_countableFiltration_countablePartitionSet

English

For each n, the function a ↦ ⟨countablePartitionSet n a, ⋯⟩ is measurable from countablePartition α n into the filtration.

Русский

Для каждого n функция a ↦ ⟨countablePartitionSet n a, ⋯⟩ измерима относительно countablePartition α n в filtration.

LaTeX

$$$$ \Measurable (a \mapsto ⟨countablePartitionSet n a, \dots⟩) $$$$

Lean4

theorem measurable_countableFiltration_countablePartitionSet (α : Type*) [MeasurableSpace α] [CountablyGenerated α]
    (n : ℕ) : Measurable[countableFiltration α n] (countablePartitionSet n) :=
  measurable_subtype_coe.comp (measurable_countablePartitionSet_subtype _ _)

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