instFunLike

Mathlib.Topology.Algebra.Module.StrongTopology

URI: https://scilib.ai/kg/mathlib#UniformConvergenceCLM.instFunLike

English

UniformConvergenceCLM inherits a FunLike structure from ContinuousLinearMap.funLike.

Русский

UniformConvergenceCLM наследует структуру FunLike из ContinuousLinearMap.funLike.

LaTeX

$$$\\text{IsFunLike}( \\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S}), E, F).$$$

Lean4

instance instFunLike [TopologicalSpace F] (𝔖 : Set (Set E)) : FunLike (UniformConvergenceCLM σ F 𝔖) E F :=
  ContinuousLinearMap.funLike

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru