English
From a FunLike Real-valued F on an additive group E and a NonarchAddGroupSeminormClass F E, there is a canonical AddGroupSeminormClass F E ℝ structure, with compatible map_add_le_add and map_neg_eq_map.
Русский
Из FunLike F E ℝ и NonarchAddGroupSeminormClass F E следует каноническая структура AddGroupSeminormClass F E ℝ, совместимая по неравенству сложения и отображению инверсия.
LaTeX
$$\\text{AddGroupSeminormClass } F E \\mathbb{R} \\,\\text{содержит } \\text{map\_add\_le\_add}, \\text{map\_neg\_eq\_map'}$$
Lean4
instance (priority := 100) toAddGroupSeminormClass [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupSeminormClass F E] :
AddGroupSeminormClass F E ℝ :=
{
‹NonarchAddGroupSeminormClass F
E› with
map_add_le_add := fun f _ _ =>
haveI h_nonneg : ∀ a, 0 ≤ f a := by
intro a
rw [← NonarchAddGroupSeminormClass.map_zero f, ← sub_self a]
exact le_trans (map_sub_le_max _ _ _) (by rw [max_self (f a)])
le_trans (map_add_le_max _ _ _)
(max_le (le_add_of_nonneg_right (h_nonneg _)) (le_add_of_nonneg_left (h_nonneg _)))
map_neg_eq_map := NonarchAddGroupSeminormClass.map_neg_eq_map' }
-- See note [lower instance priority]
