nhdsWithin_Ici_isMeasurablyGenerated

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

The neighborhood filter within the left ray Iic is measurably generated for all a.

Русский

Фильтр окрестностей внутри луча Iic является измеримо порожденным для всех a.

LaTeX

$$$\bigl(\nhdsWithin a (\,\{x \le c\}\, )\bigr).IsMeasurablyGenerated$.$$

Lean4

instance nhdsWithin_Ici_isMeasurablyGenerated : (𝓝[Ici b] a).IsMeasurablyGenerated :=
  measurableSet_Ici.nhdsWithin_isMeasurablyGenerated _

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

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

Разделы

Аффилиация

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