flip_comp — Mathlib

English

Flipping the composition distributes: flip(r ∘r p) = flip p ∘r flip r.

Русский

Переворот композиции распределяется: flip(r ∘r p) = flip p ∘r flip r.

LaTeX

$$$\mathrm{flip}(\mathrm{Relation.Comp}(r,p)) = \mathrm{Relation.Comp}(\mathrm{flip}(p), \mathrm{flip}(r))$$$

Lean4

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

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