instSMulCommClass_sphere_sphere_closedBall

English

The scalar actions from three sphere layers commute pairwise, yielding a SMulCommClass for sphere-sphere-sphere.

Русский

Действия скалярных слоев из трех сфер взаимно коммутируют, образуя SMulCommClass для sphere-sphere-sphere.

LaTeX

$$$\text{instSMulCommClass_sphere_sphere_sphere}$$$

Lean4

instance instSMulCommClass_sphere_sphere_closedBall :
    SMulCommClass (sphere (0 : 𝕜) 1) (sphere (0 : 𝕜') 1) (closedBall (0 : E) r) :=
  ⟨fun a b c => Subtype.ext <| smul_comm (a : 𝕜) (b : 𝕜') (c : E)⟩

Похожие утверждения