isVonNBounded_iff — Mathlib

English

If the neighborhood filter has a basis, IsVonNBounded is characterized by a basis indexing condition.

Русский

Если у фильтра окрестностей есть базис, тогда ограниченность Вон Невена определяется индексацией по базису.

LaTeX

$$$\\forall\\text{basis } h, IsVonNBounded 𝕜 A \\iff \\forall i, q i \\to Absorbs 𝕜 (s i) A$$$

Lean4

theorem _root_.Filter.HasBasis.isVonNBounded_iff {q : ι → Prop} {s : ι → Set E} {A : Set E}
    (h : (𝓝 (0 : E)).HasBasis q s) : IsVonNBounded 𝕜 A ↔ ∀ i, q i → Absorbs 𝕜 (s i) A :=
  by
  refine ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩
  rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩
  exact (hA i hi).mono_left hV

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