instLipschitzAddAdditiveOfLipschitzMul

Mathlib.Topology.MetricSpace.Algebra

URI: https://scilib.ai/kg/mathlib#instLipschitzAddAdditiveOfLipschitzMul

English

If α is a monoid with LipschitzMul, then the additive structure on its Additive presentation is Lipschitz.

Русский

Если α — моноид с LipschitzMul, то для аддитивной структуры на Additive α выполняется Lipschitz.

LaTeX

$$LipschitzAdd (Additive α)$$

Lean4

instance [Monoid α] [LipschitzMul α] : LipschitzAdd (Additive α) :=
  ⟨@LipschitzMul.lipschitz_mul α _ _ _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru