continuousAt_infty — Mathlib

English

A map f: OnePoint X → Y is continuous at ∞ iff for every neighborhood s of f(∞), there exists a closed, compact t ⊆ X such that f maps the complement of t into s.

Русский

Непрерывность в ∞ эквивалентна тому, что для каждого окрестного множества s вокруг f(∞) существует замкнутое компактное t ⊆ X такое, что f(X\t) ⊆ s.

LaTeX

$$$\text{ContinuousAt } f(\infty) \iff \forall s \in 𝓝(f(\infty)), \exists t: Set X, IsClosed t \land IsCompact t \land MapsTo (f \circ (↑)) t^{c} s$$$

Lean4

theorem continuousAt_infty {Y : Type*} [TopologicalSpace Y] {f : OnePoint X → Y} :
    ContinuousAt f ∞ ↔ ∀ s ∈ 𝓝 (f ∞), ∃ t : Set X, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ (↑)) tᶜ s :=
  continuousAt_infty'.trans <| by simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]

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