tendsto_atTop_embedding — Mathlib

English

Let e be an order-embedding with a cofinal property. Then Tendsto (e ∘ f) l atTop is equivalent to Tendsto f l atTop.

Русский

Пусть e — вложение по порядку с кофинальной характеристикой. Тогда Tendsto (e ∘ f) l atTop эквивалентно Tendsto f l atTop.

LaTeX

$$$\operatorname{Tendsto}(e \circ f) \; l\; \operatorname{atTop} \iff \operatorname{Tendsto} f \; l \; \operatorname{atTop}$$$

Lean4

theorem tendsto_atTop_embedding [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, c ≤ e b) : Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop := by
  rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

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