English
Any action on ℝ which factors through ℝ≥0 applies to a NonarchAddGroupSeminorm, i.e., there is a compatible SMul action of a scalar ring on NonarchAddGroupSeminorm E.
Русский
Любое действие на ℝ, которое факorizируется через ℝ≥0, применяется к NonarchAddGroupSeminorm, то есть существует совместное действие скаляра на NonarchAddGroupSeminorm E.
LaTeX
$$$ \text{SMul } R ( \mathrm{NonarchAddGroupSeminorm} E ) $$$
Lean4
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to a `NonarchAddGroupSeminorm`. -/
instance : SMul R (NonarchAddGroupSeminorm 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 p, mul_zero]
add_le_max' := fun x y =>
by
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul,
← mul_max_of_nonneg _ _ NNReal.zero_le_coe]
gcongr
apply map_add_le_max
neg' := fun x => by simp_rw [map_neg_eq_map p] }⟩
