instContinuousMapClass — Mathlib

English

There is a typeclass indicating that NormedAddGroupHom acts as a class of continuous maps between normed groups.

Русский

Существaет типовый класс, обозначающий, что NormedAddGroupHom образует класс непрерывных отображений между нормированными группами.

LaTeX

$$$\\text{instance }\\text{ContinuousMapClass}(NormedAddGroupHom\,V_1\,V_2)\,V_1\,V_2$$$

Lean4

instance : ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂ where map_continuous := fun f => f.continuous

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