English
Let f: α → β be a function with β having no maximum, and l a nonempty directed filter, if f tends to atTop along l, then f is not bounded above along l.
Русский
Пусть f: α → β, где β не имеет максимального элемента, и l — ненулевой направленный фильтр; если f стремится к бесконечности вдоль l, то f не ограничен сверху вдоль l.
LaTeX
$$$ (hf : Tendsto f l atTop) \Rightarrow \neg IsBoundedUnder (\le) l f $$$
Lean4
theorem not_isBoundedUnder_of_tendsto_atTop [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} [l.NeBot]
(hf : Tendsto f l atTop) : ¬IsBoundedUnder (· ≤ ·) l f :=
by
rintro ⟨b, hb⟩
rw [eventually_map] at hb
obtain ⟨b', h⟩ := exists_gt b
have hb' := (tendsto_atTop.mp hf) b'
have : {x : α | f x ≤ b} ∩ {x : α | b' ≤ f x} = ∅ :=
eq_empty_of_subset_empty fun x hx => (not_le_of_gt h) (le_trans hx.2 hx.1)
exact (nonempty_of_mem (hb.and hb')).ne_empty this
