continuousAt_infty' — Mathlib

English

A map f: OnePoint X → Y is continuous at ∞ iff Tendsto (f ∘ ↑) from coclosedCompact X to nhds (f ∞).

Русский

Элемент карты f бесконечной точке ∞ непрерывно в точке ∞ тогда, когда предел f по ограничению на X существует: Tendsto (f ∘ ι) от coclosedCompact X к nhds (f ∞).

LaTeX

$$$\forall {f: OnePoint X \to Y},\ (ContinuousAt f \infty) \iff (Tendsto (f \circ (\uparrow)) (coclosedCompact X) (\mathcal{N}(f(\infty))))$$$

Lean4

theorem continuousAt_infty' {Y : Type*} [TopologicalSpace Y] {f : OnePoint X → Y} :
    ContinuousAt f ∞ ↔ Tendsto (f ∘ (↑)) (coclosedCompact X) (𝓝 (f ∞)) :=
  tendsto_nhds_infty'.trans <| and_iff_right (tendsto_pure_nhds _ _)

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