uniformity_toTopologicalSpace_eq — Mathlib

English

Equality of the topological space structure in the uniform convergence setting with its induced form.

Русский

Равенство структуры топологического пространства в настройке равномерной сходимости с индуцированной формой.

LaTeX

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

Lean4

@[simp]
theorem uniformity_toTopologicalSpace_eq [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    (UniformConvergenceCLM.instUniformSpace σ F 𝔖).toTopologicalSpace =
      UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 :=
  rfl

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