mulActionClosedBallClosedBall — Mathlib

English

Similarly, there is a multiplicative action of the closedBall on the closedBall that respects the closedBall bounds.

Русский

Аналогично, существует действие на замкнутом шаре, сохраняющее границы шаров.

LaTeX

$$$\\text{MulAction}(\\text{closedBall}(0,1), \\text{closedBall}(0,r))$ with the multiplication well-defined coordinatewise.$$

Lean4

instance mulActionClosedBallClosedBall : MulAction (closedBall (0 : 𝕜) 1) (closedBall (0 : E) r)
    where
  smul c
    x :=
    ⟨(c : 𝕜) • ↑x,
      mem_closedBall_zero_iff.2 <| by
        simpa only [norm_smul, one_mul] using
          mul_le_mul (mem_closedBall_zero_iff.1 c.2) (mem_closedBall_zero_iff.1 x.2) (norm_nonneg _) zero_le_one⟩
  one_smul _ := Subtype.ext <| one_smul 𝕜 _
  mul_smul _ _ _ := Subtype.ext <| mul_smul _ _ _

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