comap_dist_right_atTop — Mathlib

English

The comap of the distance to c is equal to cobounded, mirroring the right-atTop case.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comap_dist_right_atTop (c : α) : comap (dist · c) atTop = cobounded α :=
  (atTop_basis.comap _).eq_of_same_basis <| by
    simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c

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