instSemigroup — Mathlib

English

The closed unit ball is a semigroup under multiplication: the product of any two elements in the closed ball remains in the closed ball.

Русский

Замкнутая единичная сфера образует полугруппу под умножением: произведение любых двух элементов внутри замкнутого шара остается внутри шара.

LaTeX

$$$\\forall x,y \\in \\overline{\\text{Ball}}(0,1),\\; x\\cdot y \\in \\overline{\\text{Ball}}(0,1)$$$

Lean4

instance instSemigroup [NonUnitalSeminormedRing 𝕜] : Semigroup (closedBall (0 : 𝕜) 1) :=
  MulMemClass.toSemigroup (Subsemigroup.unitClosedBall 𝕜)

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