mulActionSphereBall — Mathlib

English

The scalar action of the sphere on the ball is continuous with respect to the subspace/topology.

Русский

Действие сферы на шар непрерывно в топологическом смысле.

LaTeX

$$$\\text{continuousSMul}_{SphereBall}$$$

Lean4

instance mulActionSphereBall : MulAction (sphere (0 : 𝕜) 1) (ball (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 _ _ _

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