tendsto_ofReal_cobounded_cobounded

English

For any 𝕜 with RCLike, the map ofReal: ℝ → 𝕜 sends cobounded sets to cobounded sets in the sense of Tendsto.

Русский

Для 𝕜 типа RCLike отображение ofReal переводит cobounded множества в cobounded через пределы Tendsto.

LaTeX

$$$\text{Tendsto} \mathrm{ofReal} (\text{cobounded } \mathbb{R}) (\text{cobounded } 𝕜)$$$

Lean4

theorem tendsto_ofReal_cobounded_cobounded : Tendsto ofReal (Bornology.cobounded ℝ) (Bornology.cobounded 𝕜) :=
  tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_norm_cobounded_atTop)

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