eventually_forall_le_atBot — Mathlib

English

Dual of AtTopGe with atBot: if f tends to atBot and p holds eventually on atBot, then eventually for all y with y ≤ f(x) we have p(y).

Русский

Двойственность к AtTopGe: если f стремится к atBot и p выполняется рано или поздно на atBot, тогда рано или поздно для всех y с y ≤ f(x) выполняется p(y).

LaTeX

$$$\text{Tendsto}(f, l, \operatorname{atBot}) \Rightarrow (\forall^\infty x \in \operatorname{atBot}, p(x)) \Rightarrow \forall^\infty x \in l, \forall y, y \le f(x) \Rightarrow p(y)$$$

Lean4

theorem eventually_forall_le_atBot [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Tendsto f l atBot)
    (h_evtl : ∀ᶠ x in atBot, p x) : ∀ᶠ x in l, ∀ y, y ≤ f x → p y := by
  rw [← Filter.eventually_forall_le_atBot] at h_evtl; exact (h_evtl.comap f).filter_mono hf.le_comap

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