instMonoid — Mathlib

English

The set of RelEmbedding r r forms a monoid under composition, with identity as the unit.

Русский

Множество RelEmbedding r r образует моноид по композиции, единица — тождественный отображение.

LaTeX

$$(\text{RelEmbedding}(r,r), \cdot, \mathrm{id}) \text{ is a monoid; } f \cdot g = g \circ f$$

Lean4

instance : Monoid (r ↪r r) where
  one := .refl r
  mul f g := g.trans f
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl

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