comp_assoc — Mathlib

English

Relation composition is associative: (r ∘r p) ∘r q = r ∘r p ∘r q.

Русский

Осторожно: композиция отношений ассоциативна: (r ∘r p) ∘r q = r ∘r p ∘r q.

LaTeX

$$$(r \circ_r p) \circ_r q = r \circ_r p \circ_r q$$$

Lean4

theorem comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q := by
  funext a d
  apply propext
  constructor
  · exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
  · exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

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