exists_lt_of_tendsto_atBot — Mathlib

English

Assume NoMaxOrder on β and Tendsto u atTop atTop. Then for every a,b there exists a' ≥ a with b < u(a').

Русский

Пусть β имеет NoMaxOrder и Tendsto u от atTop к atTop. Тогда для каждого a,b существует a' ≥ a с b < u(a').

LaTeX

$$$[NoMaxOrder\ β]\ (h : Tendsto u\ atTop\ atTop)\to ∀ a,b, \exists a' \ge a, b < u(a')$$$

Lean4

theorem exists_lt_of_tendsto_atBot [NoMinOrder β] (h : Tendsto u atTop atBot) : ∀ a b, ∃ a' ≥ a, u a' < b :=
  exists_lt_of_tendsto_atTop (β := βᵒᵈ) h

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