eventually_le_const — Mathlib

English

If v < u and f tends to v along l, then f(a) ≤ u eventually.

Русский

Если v < u и f сходится к v вдоль фильтра l, то значения f(a) удовлетворяют f(a) ≤ u на протяжении фильтра.

LaTeX

$$$v < u \land \mathrm{Tendsto}(f, l, 𝓝 v) \rightarrow \forall^\infty a \in l, f(a) \le u$$$

Lean4

theorem eventually_le_const {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Tendsto f l (𝓝 v)) :
    ∀ᶠ a in l, f a ≤ u :=
  h.eventually <| eventually_le_nhds hv

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