hasBasis_cobounded_compl_ball — Mathlib

English

The cobounded filter has a basis consisting of the complements of balls (not necessarily closed) around center c.

Русский

Фильтр кобундированности имеет базис, состоящий из дополнений к ball c r.

LaTeX

$$$ (cobounded\;\alpha)\.HasBasis (\lambda _ => True) (\lambda r \to (ball\; c\; r)^c) $$$

Lean4

theorem hasBasis_cobounded_compl_ball (c : α) : (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (ball c r)ᶜ) :=
  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_ball c).trans <| by simp⟩

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