English
Let l be a filter on γ, f: γ → α, and u < v in α. If f tends to v along l (i.e., f(l) → v in the neighbourhood of v), then f(a) is eventually at least u; equivalently, there exists a set in l on which u ≤ f(a) holds for all a in that set.
Русский
Пусть l — фильтр на γ, f: γ → α, и u < v в линейном порядке α. Если f стремится к v по l (f(l) → v в окрестностях v), то f(a) будет не меньше u на большом подмножстве l; то есть существует множество в l, такое что для всех a в этом множестве выполняется u ≤ f(a).
LaTeX
$$$\forall {l : Filter \ γ} {f : γ \ → \alpha} {u v : \alpha},\; u < v \rightarrow Tendsto f\ l\ (\mathcal{N}\ v) \rightarrow \forall a \in l,\; u \le f(a)$$$
Lean4
theorem eventually_const_le {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Tendsto f l (𝓝 v)) :
∀ᶠ a in l, u ≤ f a :=
h.eventually <| eventually_ge_nhds hv
