tendsto_of_seq_tendsto — Mathlib

English

If for every sequence x: ℕ → α that tends to k, f ∘ x tends to l, then f tends to l along k.

Русский

Если для каждой последовательности x: ℕ → α сходящейся к k функцияe f ∘ x сходится к l, тогда f сходится к l по отношению к k.

LaTeX

$$$\\Big( \\forall x:\\mathbb{N} \\to \\alpha, \\operatorname{Tendsto} x\\, atTop\\, k \\Rightarrow \\operatorname{Tendsto}(f \\circ x)\\, atTop\\, l \\Big) \\Rightarrow \\operatorname{Tendsto} f\\, k\\, l$$$

Lean4

theorem tendsto_of_seq_tendsto {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
    (∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l) → Tendsto f k l :=
  tendsto_iff_seq_tendsto.2

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