atBot_isMeasurablyGenerated

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

URI: https://scilib.ai/kg/mathlib#atBot_isMeasurablyGenerated

← MathLib Explorer

English

The atTop filter is measurably generated.

Русский

Фильтр atTop является измеримо порожденным.

LaTeX

$$$(\text{Filter.atTop}).IsMeasurablyGenerated$.$$

Lean4

instance atBot_isMeasurablyGenerated : (Filter.atBot : Filter α).IsMeasurablyGenerated :=
  @Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Iic : MeasurableSet (Iic a)).principal_isMeasurablyGenerated

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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