mulActionSphereClosedBall — Mathlib

English

There is a natural action of the sphere on the closedBall that is compatible with the ball's metric structure.

Русский

Существует естественное действие сферы на замкнутом шаре, совместимое с метрической структурой шара.

LaTeX

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

Lean4

instance mulActionSphereClosedBall : MulAction (sphere (0 : 𝕜) 1) (closedBall (0 : E) r)
    where
  smul c x := inclusion sphere_subset_closedBall c • x
  one_smul _ := Subtype.ext <| one_smul _ _
  mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _

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