tendsto_intCast_atTop_cobounded — Mathlib

English

A parallel statement to tendsto_natCast_atTop_cobounded for Int.cast.

Русский

Похожее утверждение для Int.cast, аналогично tendsto_natCast_atTop_cobounded.

LaTeX

$$$$\\\\ Tendsto Int.cast atTop (Bornology.cobounded α) $$$$

Lean4

theorem tendsto_intCast_atTop_cobounded [NormedRing α] [NormSMulClass ℤ α] [Nontrivial α] :
    Tendsto Int.cast atTop (Bornology.cobounded α) :=
  tendsto_intCast_atBot_sup_atTop_cobounded.mono_left le_sup_right

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