eventually_lt_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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