tendsto_atTop_iff — Mathlib

English

Let e be an order isomorphism. Then for any l and f, Tendsto (e(f)) toTop iff Tendsto f toTop.

Русский

Пусть e—порядок-изоморфизм. Тогда для любых фильтра l и функции f: Tendsto (e ∘ f) к верхнему пределу эквивалентно Tendsto f к верхнему пределу.

LaTeX

$$$\\forall l:\\\\Filter \\gamma, \\forall f:\\\\gamma \\to \\alpha,\\; \\operatorname{Tendsto}(\\lambda x. e(f(x)))\,l\\,\\operatorname{atTop} \\iff \\operatorname{Tendsto} f\,l\\,\\operatorname{atTop}$$$

Lean4

@[simp]
theorem tendsto_atTop_iff {l : Filter γ} {f : γ → α} (e : α ≃o β) :
    Tendsto (fun x => e (f x)) l atTop ↔ Tendsto f l atTop := by
  rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]

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