unitClosedBall — Mathlib

English

The closed unit ball forms a monoid under multiplication: it contains 1 and is closed under multiplication.

Русский

Замкнутый шар единицы образует моноид по умножению: в нём присутствует 1 и она замкнута по умножению.

LaTeX

$$$1 \in \overline{B}(0,1) \\land\\forall x,y \in \overline{B}(0,1),\; xy \in \overline{B}(0,1)$$$

Lean4

/-- Closed unit ball in a seminormed ring as a bundled `Submonoid`. -/
def unitClosedBall (𝕜 : Type*) [SeminormedRing 𝕜] [NormOneClass 𝕜] : Submonoid 𝕜 :=
  { Subsemigroup.unitClosedBall 𝕜 with
    carrier := closedBall 0 1
    one_mem' := mem_closedBall_zero_iff.2 norm_one.le }

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