exists_le_of_tendsto_atTop — Mathlib

English

If a function u tends to the top along atTop, then for every a and b there exists a' ≥ a with b ≤ u(a').

Русский

Если функция u стремится к вершине вдоль atTop, то для любых a и b существует a' ≥ a с b ≤ u(a').

LaTeX

$$$(h : Tendsto u\ atTop\ atTop)\to ∀ a, b, \exists a' \ge a, b \le u(a')$$$

Lean4

theorem exists_le_of_tendsto_atTop (h : Tendsto u atTop atTop) (a : α) (b : β) : ∃ a' ≥ a, b ≤ u a' :=
  by
  have : Nonempty α := ⟨a⟩
  have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x := (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
  exact this.exists

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