instLipschitzMulOrderDual — Mathlib

English

Let α be a monoid with a metric for which multiplication is Lipschitz. Then the opposite monoid αᵒᵈ (with reversed multiplication) also has Lipschitz multiplication.

Русский

Пусть α — моноид с метрическим пространством так, что умножение Lipschitz. Тогда противоположный моноид αᵒᵈ (с обратным умножением) также обладает Lipschitz-умножением.

LaTeX

$$$Monoid(\\alpha) \\land LipschitzMul(\\alpha) \\Rightarrow LipschitzMul(\\alpha^{\\mathrm{op}})$$$

Lean4

@[to_additive]
instance [Monoid α] [LipschitzMul α] : LipschitzMul αᵒᵈ :=
  ‹LipschitzMul α›

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