isMeasurablyGenerated_top

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

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

English

The top filter on α is measurably generated.

Русский

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

LaTeX

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

Lean4

instance isMeasurablyGenerated_top : IsMeasurablyGenerated (⊤ : Filter α) :=
  ⟨fun _s hs => ⟨univ, univ_mem, MeasurableSet.univ, fun x _ => hs x⟩⟩

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

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

Разделы

Аффилиация

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