measurable_countablePartitionSet_subtype

English

The map n ↦ ⟨countablePartitionSet n a, countablePartitionSet_mem n a⟩ is measurable from countablePartition α n into countableFiltration α n.

Русский

Отображение n ↦ ⟨countablePartitionSet n a, countablePartitionSet_mem n a⟩ измеримо относительно countableFiltration α n.

LaTeX

$$$$ @Measurable α (countablePartition α n) (countableFiltration α n) \; m \; (\lambda a \mapsto ⟨countablePartitionSet n a, countablePartitionSet_mem n a\rangle) $$$$

Lean4

theorem measurable_countablePartitionSet_subtype (n : ℕ) (m : MeasurableSpace (countablePartition α n)) :
    @Measurable α (countablePartition α n) (countableFiltration α n) m
      (fun a ↦ ⟨countablePartitionSet n a, countablePartitionSet_mem n a⟩) :=
  measurable_memPartitionSet_subtype (measurableSet_enumerateCountable_countableGeneratingSet (α := α)) n m

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