measurableSet_natGeneratingSequence

English

Each element of the natGeneratingSequence is a measurable subset.

Русский

Каждый элемент natGeneratingSequence — измеримое подмножество.

LaTeX

$$$ \forall n, MeasurableSet (natGeneratingSequence (\alpha) n) $$$

Lean4

theorem measurableSet_natGeneratingSequence [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
    MeasurableSet (natGeneratingSequence α n) :=
  measurableSet_countableGeneratingSet <| Set.enumerateCountable_mem _ empty_mem_countableGeneratingSet n

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