English
The underlying function of the zero seminorm is the zero function: for all x, (0 : NonarchAddGroupSeminorm E) x = 0.
Русский
Базовая функция нулевого семинорма есть нулевая функция: для всех x (0 : NonarchAddGroupSeminorm E) x = 0.
LaTeX
$$$ \forall x : E,\; (0 : \mathrm{NonarchAddGroupSeminorm} E)(x) = 0 $$$
Lean4
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`. -/
instance : SMul R (GroupSeminorm E) :=
⟨fun r p =>
{ toFun := fun x => r • p x
map_one' := by
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_one_eq_zero p, mul_zero]
mul_le' := fun _ _ =>
by
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
gcongr
apply map_mul_le_add
inv' := fun x => by simp_rw [map_inv_eq_map p] }⟩
