exists_lt_of_tendsto_atTop — Mathlib

English

Let F be a filter and u: α→β. Then the NeBot of F ⊓ map u atTop is equivalent to: for every U ∈ F and any N, there exists n ≥ N with u(n) ∈ U.

Русский

Пусть F — фильтр, u: α→β. Тогда NeBot (F ⊓ map u atTop) эквивалентно: для каждого U ∈ F и любого N существует n ≥ N такой, что u(n) ∈ U.

LaTeX

$$$ NeBot\ (F \sqcap map\ u\ atTop) \iff \forall U \in F, \forall N, \exists n \ge N, u(n) \in U$$$

Lean4

theorem exists_lt_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto u atTop atTop) (a : α) (b : β) : ∃ a' ≥ a, b < u a' :=
  by
  obtain ⟨b', hb'⟩ := exists_gt b
  rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩
  exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩

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