toUniformOnFun_toFun — Mathlib

English

The underlying function of the UniformOnFun representation coincides with the original multilinear map.

Русский

Базовая функция представления UniformOnFun совпадает с исходным мультилинеарным отображением.

LaTeX

$$$\text{UniformOnFun.toFun}(\text{toUniformOnFun}(f)) = f$$$

Lean4

@[simp]
theorem toUniformOnFun_toFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
    UniformOnFun.toFun _ f.toUniformOnFun = f :=
  rfl

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