topologicalSpace_eq — Mathlib

English

Equality of the topological space on UniformConvergenceCLM with its induced form via the FunLike/coercion.

Русский

Равенство топологического пространства на UniformConvergenceCLM с его индуцированной формой через FunLike/коэрццию.

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

theorem topologicalSpace_eq [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    instTopologicalSpace σ F 𝔖 =
      TopologicalSpace.induced (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖) :=
  by
  rw [instTopologicalSpace]
  congr
  exact IsUniformAddGroup.toUniformSpace_eq

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