tendsto_atBot_embedding — Mathlib

English

Dual to tendsto_atTop_embedding: Tendsto (e ∘ f) l atBot iff Tendsto f l atBot, under a suitable embedding e.

Русский

Дуально к предыдущему: Tendsto (e ∘ f) l atBot ⇔ Tendsto f l atBot при подходящем вложении.

LaTeX

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

Lean4

/-- A function `f` goes to `-∞` independent of an order-preserving embedding `e`. -/
theorem tendsto_atBot_embedding [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, e b ≤ c) : Tendsto (e ∘ f) l atBot ↔ Tendsto f l atBot :=
  @tendsto_atTop_embedding α βᵒᵈ γᵒᵈ _ _ f e l (Function.swap hm) hu

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