instTopologicalSpace — Mathlib

English

The topology on UniformConvergenceCLM σ F 𝔖 is the induced topology via the evaluation map from E →ᵤ[𝔖] F.

Русский

Топология на UniformConvergenceCLM σ F 𝔖 задаётся как индуцированная топология по отображению оценки из E →ᵤ[𝔖] F.

LaTeX

$$$\\text{instTopologicalSpace}(\\sigma,F,\\mathcal{S}) = \\mathrm{TopologicalSpace.induced}(\\mathrm{UniformOnFun.ofFun}\\,\\mathcal{S} \\circ \\mathrm{DFunLike.coe},\\, \\mathrm{UniformOnFun.topologicalSpace} E F 𝔖).$$$

Lean4

instance instTopologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) :
    TopologicalSpace (UniformConvergenceCLM σ F 𝔖) :=
  (@UniformOnFun.topologicalSpace E F (IsTopologicalAddGroup.toUniformSpace F) 𝔖).induced
    (DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → (E →ᵤ[𝔖] F))

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