hasAntitoneBasis_cobounded_compl_closedBall

English

The cobounded filter has an antitone basis given by r ↦ (ball c r)^c, i.e., larger radii yield smaller complements.

Русский

Фильтр кобундированности обладает антиинтонным базисом, задаваемым r ↦ (ball c r)^c: больший радиус даёт меньшие дополнения.

LaTeX

$$$ (cobounded\;\alpha) \.HasAntitoneBasis (\lambda r \mapsto (ball\; c\; r)^c) $$$

Lean4

theorem hasAntitoneBasis_cobounded_compl_closedBall (c : α) :
    (cobounded α).HasAntitoneBasis (fun r ↦ (closedBall c r)ᶜ) :=
  ⟨Metric.hasBasis_cobounded_compl_closedBall _, fun _ _ hr _ ↦ by simpa using hr.trans_lt⟩

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