C — Mathlib · SciLib

English

For a monoid β with LipschitzMul structure, the Lipschitz constant Cβ is the Lipschitz bound for the multiplication map (x,y) ↦ xy.

Русский

Для моноида β с образом LipschitzMul константа Липшица Cβ задаёт предел Липшца для отображения умножения (x,y)↦xy.

LaTeX

$$$C_\\beta := \\text{Lipschitz constant of }(x,y)\\mapsto xy$ for a LipschitzMul β.$$

Lean4

/-- The Lipschitz constant of a monoid `β` satisfying `LipschitzMul` -/
@[to_additive /-- The Lipschitz constant of an `AddMonoid` `β` satisfying `LipschitzAdd` -/
    ]
def C [_i : LipschitzMul β] : ℝ≥0 :=
  Classical.choose _i.lipschitz_mul

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