inv_comp — Mathlib

English

Let R: SetRel α β and S: SetRel β γ. The inverse of the composite equals the composite of the inverses in reverse order: (R ○ S).inv = S.inv ○ R.inv.

Русский

Пусть R: SetRel α β и S: SetRel β γ. Обратная композиция равна композиции обратных отношений в обратном порядке: (R ○ S).inv = S.inv ○ R.inv.

LaTeX

$$$ (R \circ S)^{-1} = S^{-1} \circ R^{-1} $$$

Lean4

@[simp]
theorem inv_comp (R : SetRel α β) (S : SetRel β γ) : (R ○ S).inv = S.inv ○ R.inv := by aesop

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