tendsto_add_atTop_nat — Mathlib

English

For any k ∈ ℕ, the function a ↦ a + k preserves atTop as a filter: Tendsto a ↦ a + k along atTop to atTop.

Русский

Для любого k ∈ ℕ отображение a ↦ a + k сохраняет atTop: предел по atTop равен atTop.

LaTeX

$$$$\operatorname{Tendsto}(\lambda a. a + k)\;\operatorname{atTop}\; \operatorname{atTop}$$$$

Lean4

theorem tendsto_add_atTop_nat (k : ℕ) : Tendsto (fun a => a + k) atTop atTop :=
  le_of_eq (map_add_atTop_eq_nat k)

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