instMonoid — Mathlib

English

The set of endomorphisms of a relation r on α, RelIso r r, forms a monoid under composition with identity.

Русский

Множество изоморфизмов отношений RelIso r r образует моноид под операцией композиции с единицей как тождественный образ.

LaTeX

$$(\text{RelIso}(r,r), \cdot, \mathrm{id}_r) \text{ is a monoid} \\text{ with } f \cdot g = g \circ f$$

Lean4

instance : Monoid (r →r r) where
  one := .id r
  mul := .comp
  mul_assoc _ _ _ := rfl
  one_mul _ := rfl
  mul_one _ := rfl

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