mulActionClosedBallBall — Mathlib

English

There is a natural action of the sphere of radius 1 in 𝕜 on the ball of radius r in E by pointwise multiplication, preserving the ball structure.

Русский

Сфера радиуса 1 в 𝕜 действует на шар радиуса r в E по точечной умножению, сохраняет шаровую структуру.

LaTeX

$$$\\text{MulAction}(\\text{sphere}(0,1), \\text{ball}(0,r))$ with the smul defined by inclusion and scalar multiplication in each coordinate.$$

Lean4

instance mulActionClosedBallBall : MulAction (closedBall (0 : 𝕜) 1) (ball (0 : E) r)
    where
  smul c
    x :=
    ⟨(c : 𝕜) • ↑x,
      mem_ball_zero_iff.2 <| by
        simpa only [norm_smul, one_mul] using
          mul_lt_mul' (mem_closedBall_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) (norm_nonneg _) one_pos⟩
  one_smul _c₂ := Subtype.ext <| one_smul 𝕜 _
  mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _

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