measurableSet_enumerateCountable_countableGeneratingSet

English

For a countably generated space, the set enumerated by enumerateCountable over the empty set is measurable at every stage n.

Русский

Для пространства с счётной порождаемостью множество, получаемое enumerateCountable над пустым множеством, измеримо на каждом шаге n.

LaTeX

$$$\\MeasurableSet\\big(\\text{enumerateCountable}(\\text{countable\_generatingSet})\\, \\emptyset \\ n\\big)$$$

Lean4

theorem measurableSet_enumerateCountable_countableGeneratingSet (α : Type*) [MeasurableSpace α] [CountablyGenerated α]
    (n : ℕ) : MeasurableSet (enumerateCountable (countable_countableGeneratingSet (α := α)) ∅ n) :=
  measurableSet_countableGeneratingSet (enumerateCountable_mem _ (empty_mem_countableGeneratingSet) n)

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