cobounded_of_norm' — Mathlib

English

If a filter has a basis atTop, the cobounded filter has a corresponding basis given by the norm preimages of those sets.

Русский

Если фильтр имеет базис на бесконечности, то cobounded имеет аналогичный базис, задаваемый через предобраз норм по тем же множествам.

LaTeX

$$HasBasis (cobounded E) p (i ↦ norm^{-1}' s i)$$

Lean4

@[to_additive Filter.HasBasis.cobounded_of_norm]
theorem cobounded_of_norm' {ι : Sort*} {p : ι → Prop} {s : ι → Set ℝ} (h : HasBasis atTop p s) :
    HasBasis (cobounded E) p fun i ↦ norm ⁻¹' s i :=
  comap_norm_atTop' (E := E) ▸ h.comap _

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