nhdsWithin_Ioi_isMeasurablyGenerated

English

For all a,b in α with a linear order and a topology, the filter 𝓝[Ioi b] a is generated by measurable sets; i.e., it is measurably generated.

Русский

Для всех a,b в α с упорядочением и топологией фильтр 𝓝[Ioi b] a состоит из измеримо сгенерируемых множеств; т.е. он измеримо сгенерирован.

LaTeX

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

Lean4

instance nhdsWithin_Ioi_isMeasurablyGenerated : (𝓝[Ioi b] a).IsMeasurablyGenerated :=
  measurableSet_Ioi.nhdsWithin_isMeasurablyGenerated _

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