hasBasis_cobounded_compl_closedBall

English

The cobounded filter has a basis consisting of the complements of closed balls about any center c.

Русский

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

LaTeX

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

Lean4

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

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