instSemigroup

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ico.instSemigroup

English

The set Ico(0,1) with multiplication is a semigroup: the product is associative.

Русский

Множество Ico(0,1) с умножением образует полугруппу: умножение ассоциативно.

LaTeX

$$∀ p,q,r ∈ Ico(0,1), (p q) r = p (q r)$$

Lean4

instance instSemigroup : Semigroup (Ico (0 : R) 1) :=
  fast_instance%Subtype.coe_injective.semigroup _ coe_mul

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

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

Разделы

Аффилиация

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