toAddGroupNormClass — Mathlib

English

From NonarchAddGroupNormClass F E and a Real-valued FunLike F E, there is a AddGroupNormClass F E ℝ structure carrying the same map_add_le_add and map_neg_eq_map.

Русский

Из NonarchAddGroupNormClass F E и Real-valued FunLike F E следует AddGroupNormClass F E ℝ со свойствами map_add_le_add и map_neg_eq_map.

LaTeX

$$\\text{AddGroupNormClass } F E \\mathbb{R} \\,\\text{содержа } \\text{map\_add\_le\_add}, \\text{map\_neg\_eq\_map}$$

Lean4

instance (priority := 100) toAddGroupNormClass [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupNormClass F E] :
    AddGroupNormClass F E ℝ :=
  { ‹NonarchAddGroupNormClass F E› with
    map_add_le_add := map_add_le_add
    map_neg_eq_map := NonarchAddGroupSeminormClass.map_neg_eq_map' }

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