English
A refined decomposition of tendsto to ∞: Tendsto f to ∞ is equivalent to Tendsto f on the infinity boundary along pure ∞ and Tendsto f∘OnePoint.some along coclosedCompact.
Русский
Уточненная запись сходимости к ∞: Tendsto f к ∞ эквивалентно Tendsto f на границе бесконечности в сочетании с Tendsto f∘OnePoint.some вдоль coclosedCompact.
LaTeX
$$$\forall {f: OnePoint X \to \alpha},\ (Tendsto f (𝓝 ∞) l) \iff (Tendsto f (pure ∞) l ∧ Tendsto (f \circ (OnePoint.some)) (coclosedCompact X) l)$$$
Lean4
theorem tendsto_nhds_infty {α : Type*} {f : OnePoint X → α} {l : Filter α} :
Tendsto f (𝓝 ∞) l ↔ ∀ s ∈ l, f ∞ ∈ s ∧ ∃ t : Set X, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ (↑)) tᶜ s :=
tendsto_nhds_infty'.trans <| by
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and, and_assoc]
