English
The action of a scalar r on AddGroupSeminorm p yields a seminorm r • p with the expected linearity properties.
Русский
Действие скаляра r на AddGroupSeminorm p задаёт полинорму r • p и обладает линейностью.
LaTeX
$$$ (r \cdot p)(x) = r \cdot p(x) $ for all x.$$
Lean4
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`. -/
instance toSMul : SMul R (AddGroupSeminorm E) :=
⟨fun r p =>
{ toFun := fun x => r • p x
map_zero' := by simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero, mul_zero]
add_le' := fun _ _ =>
by
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
gcongr
apply map_add_le_add
neg' := fun x => by simp_rw [map_neg_eq_map] }⟩
