toUniformOnFunIsCompact — Mathlib

English

A map into the space of continuous maps is continuous iff it is continuous when viewed as a map into the UniformOnFun space.

Русский

Отображение в пространство непрерывных отображений непрерывно тогда и только тогда, когда оно непрерывно как отображение в пространство UniformOnFun.

LaTeX

$$$$ Continuous f \\iff Continuous (\\lambda x, ofFun{K|IsCompact K} (f x)). $$$$

Lean4

/-- Interpret a bundled continuous map as an element of `α →ᵤ[{K | IsCompact K}] β`.

We use this map to induce the `UniformSpace` structure on `C(α, β)`. -/
def toUniformOnFunIsCompact (f : C(α, β)) : α →ᵤ[{K | IsCompact K}] β :=
  UniformOnFun.ofFun {K | IsCompact K} f

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