tendsto_comp_val_Ici_atTop — Mathlib

English

Same as above, with a direct equivalence expressed as a lemma about tendsto with Ici.

Русский

То же самое, с эквивалентностью в виде леммы о tendsto для Ici.

LaTeX

$$$\mathrm{Tendsto}\ (f\circ \mathrm{inclusion})\ atTop\ l \iff \mathrm{Tendsto}\ f\ atTop\ l$$$

Lean4

@[simp]
theorem tendsto_comp_val_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)] {a : α} {f : α → β} {l : Filter β} :
    Tendsto (fun x : Ici a => f x) atTop l ↔ Tendsto f atTop l := by
  rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]

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