nhdsWithin_Iio_isMeasurablyGenerated

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

Similarly, the filter 𝓝[Iio b] a is measurably generated under the same assumptions.

Русский

Аналогично, фильтр 𝓝[Iio b] a измеримо сгенерирован при тех же предпосылках.

LaTeX

$$$(\mathcal{N}_{a}\, (\mathsf{Iio}(b))).\text{IsMeasurablyGenerated}$$$

Lean4

instance nhdsWithin_Iio_isMeasurablyGenerated : (𝓝[Iio b] a).IsMeasurablyGenerated :=
  measurableSet_Iio.nhdsWithin_isMeasurablyGenerated _

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

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

Разделы

Аффилиация

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