instSemigroup — Mathlib

English

For x,y in the unit ball of 𝕜, the product x*y lies again in the unit ball, and the embedding respects multiplication.

Русский

Для любых x,y из единичной сферы 𝕜 произведение x*y снова принадлежит единичной сфере, и вложение сохраняет умножение.

LaTeX

$$$\\forall x,y \\in (\\text{ball}(0,1)):\\; x\\,y \\in \\text{ball}(0,1)$$$

Lean4

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

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