empty_mem_countableGeneratingSet

Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

URI: https://scilib.ai/kg/mathlib#MeasurableSpace.empty_mem_countableGeneratingSet

English

The empty set belongs to the countableGeneratingSet α.

Русский

Пустое множество принадлежит countableGeneratingSet α.

LaTeX

$$$ \emptyset \in \text{countableGeneratingSet}(\alpha) $$$

Lean4

theorem empty_mem_countableGeneratingSet [MeasurableSpace α] [CountablyGenerated α] : ∅ ∈ countableGeneratingSet α :=
  mem_insert _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru