isScalarTower_sphere_closedBall_closedBall

English

The nested scalar actions between spheres are compatible, forming a consistent tower on ball-like sets.

Русский

Взаимодействие скалярных действий между сферами совместимо, образуя последовательную башню на шарах.

LaTeX

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

Lean4

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

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