isMeasurablyGenerated_bot

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

URI: https://scilib.ai/kg/mathlib#Filter.isMeasurablyGenerated_bot

English

The bottom filter on α is measurably generated.

Русский

Нижний фильтр на пространстве α является измеримо порожденным.

LaTeX

$$$IsMeasurablyGenerated (\\\\perp : Filter α)$$$

Lean4

instance isMeasurablyGenerated_bot : IsMeasurablyGenerated (⊥ : Filter α) :=
  ⟨fun _ _ => ⟨∅, mem_bot, MeasurableSet.empty, empty_subset _⟩⟩

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

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

Разделы

Аффилиация

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