Theorems · Theorem · functional analysis

SeminormClass.map_smul_eq_mul

∀ {F : Type u_12} {𝕜 : outParam (Type u_13)} {E : outParam (Type u_14)} {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E}
  {inst_2 : SMul 𝕜 E} {inst_3 : FunLike F E ℝ} [self : SeminormClass F 𝕜 E] (f : F) (a : 𝕜) (x : E),
  f (a • x) = ‖a‖ * f x

The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

Defined in

Mathlib.Analysis.Seminorm

Cited by

25 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormClass