isClosed_setOf_continuous — Mathlib

English

The set of continuous functions is closed in the uniform convergence topology; equivalently, the set { f : α →ᵤ β | Continuous (toFun f) } is closed.

Русский

Множество непрерывных функций замкнуто в топологии равномерной конвергенции.

LaTeX

$$$$ \{ f: α \to^{u} β \;|\; \text{Continuous}(\text{toFun}(f)) \} \text{ is closed. } $$$$

Lean4

/-- The set of continuous functions is closed in the uniform convergence topology.
This is a simple wrapper over `TendstoUniformly.continuous`. -/
theorem isClosed_setOf_continuous [TopologicalSpace α] : IsClosed {f : α →ᵤ β | Continuous (toFun f)} :=
  by
  refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_
  rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf
  exact huf.continuous (le_principal_iff.mp hu)

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