ofCompact — Mathlib

English

If α is compact, any FunLike G α β that is a ContinuousMapClass yields a ZeroAtInftyContinuousMapClass G α β.

Русский

Если α компактно, любой класс непрерывных отображений G α β может быть превращён в ZeroAtInftyContinuousMapClass G α β.

LaTeX

$$$ [CompactSpace α] \Rightarrow ZeroAtInftyContinuousMapClass G α β $$$

Lean4

/-- A continuous function on a compact space is automatically a continuous function vanishing at
infinity. This is not an instance to avoid type class loops. -/
theorem ofCompact {G : Type*} [FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α] :
    ZeroAtInftyContinuousMapClass G α β where
  map_continuous := map_continuous
  zero_at_infty := by simp

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