mulActionSphereSphere — Mathlib

English

Let the unit sphere in 𝕜 act on the ball of radius r in E by scalar multiplication; the action forms a valid multiplicative action of the sphere on the ball.

Русский

Пусть единичная сфера в 𝕜 действует на шар радиуса r в E скалярным умножением; образуется допустимое умножение сферы на шар.

LaTeX

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

Lean4

instance mulActionSphereSphere : MulAction (sphere (0 : 𝕜) 1) (sphere (0 : E) r)
    where
  smul c
    x :=
    ⟨(c : 𝕜) • ↑x,
      mem_sphere_zero_iff_norm.2 <| by
        rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop, one_mul]⟩
  one_smul _ := Subtype.ext <| one_smul _ _
  mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _

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