tendsto_ratCast_atBot_iff — Mathlib

English

Analogous to the Top case, Tendsto of f cast from ℚ to R atBot is equivalent to Tendsto f atBot.

Русский

Аналогично верхнему случаю, предельность функции, приводимая из ℚ в R в нижний фильтр, эквивалентна предельности самой функции в нижнем фильтре.

LaTeX

$$$\\operatorname{Tendsto}((f(n) : R))\, l\, \\mathrm{atBot} \\;\\Longleftrightarrow\\; \\operatorname{Tendsto} f\, l\, \\mathrm{atBot}$$$

Lean4

theorem tendsto_ratCast_atBot_iff [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot := by
  rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]; rfl

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