isClosed_setOf_continuous — Mathlib

English

If 𝔖 coheres with α, the set of 𝔖-continuous functions is closed in the 𝔖-convergence topology.

Русский

Если 𝔖 совместим с α, множество 𝔖‑непрерывных функций замкнуто в топологии 𝔖‑сходимости.

LaTeX

$$IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)}$$

Lean4

/-- Suppose that the topology on `α` is defined by its restrictions to the sets of `𝔖`.

Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of `𝔖`. -/
theorem isClosed_setOf_continuous [TopologicalSpace α] (h : IsCoherentWith 𝔖) :
    IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)} :=
  by
  refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_
  rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf
  exact (huf s hs).continuousOn <| hu fun _ ↦ Continuous.continuousOn

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