instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc

English

There is an AddMonoidHomClass for the subtype of functions with NormNoninc, between the carrier types.

Русский

Существует класс AddMonoidHom для подтипа функций NormNoninc между носителями.

LaTeX

$$AddMonoidHomClass { f : Subtype fun f => f.NormNoninc } X.carrier Y.carrier$$

Lean4

instance (X Y : SemiNormedGrp₁) : AddMonoidHomClass { f : NormedAddGroupHom X Y // f.NormNoninc } X Y
    where
  map_add f := map_add f.1
  map_zero f := map_zero f.1

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