English
In general, if a limit exists, there is a tail of the domain whose image is bounded.
Русский
В общем случае, если существует предел, существует хвост области определения, образ которого ограничен.
LaTeX
$$$\\\\forall {l:\\\\text{Filter } α} {f: α \\\\to β} {x: β}, \\\\ Tendsto f l (nhds x) \\\\Rightarrow \\\\Exists s, s \\in l \\wedge IsBounded(image f s).$$$
Lean4
/-- If a function is continuous within a set `s` at every point of a compact set `k`, then it is
bounded on some open neighborhood of `k` in `s`. -/
theorem exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt [TopologicalSpace β] {k s : Set β}
{f : β → α} (hk : IsCompact k) (hf : ∀ x ∈ k, ContinuousWithinAt f s x) :
∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' (t ∩ s)) :=
by
have : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α)) :=
by
rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
exact fun x hx ↦ disjoint_left_comm.2 <| tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)
rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this with
⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩
refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩
rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]
