nhdsWithin_uIcc_isMeasurablyGenerated

English

For all a,b,x in α, the neighborhood filter 𝓝 within x of the closed interval uIcc(a,b) is measurably generated.

Русский

Для любых a,b,x в α фильтр окрестностей 𝓝 внутри x от зажатого интервала uIcc(a,b) измеримо сгенерирован.

LaTeX

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

Lean4

instance nhdsWithin_uIcc_isMeasurablyGenerated : IsMeasurablyGenerated (𝓝[[[a, b]]] x) :=
  nhdsWithin_Icc_isMeasurablyGenerated

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