isScalarTower_sphere_closedBall_ball

English

The scalar action among sphere, closedBall, and ball is coherent, yielding associativity when composed.

Русский

Скалярное действие сферы, замкнутого шара и шара согласовано, образуя ассоциативность при композиции.

LaTeX

$$$\text{IsScalarTower}(\text{sphere}(0,1),\ \text{closedBall}(0,1),\ \text{ball}(0,r))$$$

Lean4

instance isScalarTower_sphere_closedBall_ball :
    IsScalarTower (sphere (0 : 𝕜) 1) (closedBall (0 : 𝕜') 1) (ball (0 : E) r) :=
  ⟨fun a b c => Subtype.ext <| smul_assoc (a : 𝕜) (b : 𝕜') (c : E)⟩

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