tendsto_dist_right_cobounded_atTop

English

Tendsto dist x c from x to cobounded α converges to atTop.

Русский

Сходимость расстояния от x к c по мере x в cobounded α достигает atTop.

LaTeX

$$$\operatorname{Tendsto}(\lambda x \mapsto \operatorname{dist}(x, c)) (\operatorname{cobounded}(\alpha)) \operatorname{(atTop)}$$$

Lean4

theorem tendsto_dist_right_cobounded_atTop (c : α) : Tendsto (dist · c) (cobounded α) atTop :=
  tendsto_iff_comap.2 (comap_dist_right_atTop c).ge

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