hasAntitoneBasis_cobounded_compl_ball

English

The comap of the distance to c under the atTop filter equals the cobounded filter.

Русский

Обратное отображение расстояния до c по фильтру atTop равно фильтру кобундирования.

LaTeX

$$$ comap (dist\,\cdot\, c)\; atTop = cobounded(\alpha) $$$

Lean4

theorem hasAntitoneBasis_cobounded_compl_ball (c : α) : (cobounded α).HasAntitoneBasis (fun r ↦ (ball c r)ᶜ) :=
  ⟨Metric.hasBasis_cobounded_compl_ball _, fun _ _ hr _ ↦ by simpa using hr.trans⟩

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