atTop_isMeasurablyGenerated — Mathlib

English

The filter of neighborhoods within the closed interval Icc is measurably generated.

Русский

Фильтр окрестностей внутри замкнутого интервала Icc измеримо порожден.

LaTeX

$$$ (\nhdsWithin x (Icc a b)).IsMeasurablyGenerated$.$$

Lean4

instance atTop_isMeasurablyGenerated : (Filter.atTop : Filter α).IsMeasurablyGenerated :=
  @Filter.iInf_isMeasurablyGenerated _ _ _ _ fun a =>
    (measurableSet_Ici : MeasurableSet (Ici a)).principal_isMeasurablyGenerated

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