eventually_forall_ge_atTop — Mathlib

English

If f tends to atTop and p holds eventually on atTop, then eventually for all y ≥ f(x) we have p(y).

Русский

Если f стремится к +∞ и p выполняется рано или поздно на atTop, то в пределе x находится p(y) для всех y, большего чем f(x).

LaTeX

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

Lean4

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

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