Composition_of_Relations_is_Associative
Provedcomposite-relationsproofwiki
The composition of relations is an associative binary operation
Preamble
import Mathlib.Order.RelClasses
Formal statement
theorem Composition_of_Relations_is_Associative {α β γ δ : Type*} (R₁ : α → β → Prop) (R₂ : β → γ → Prop) (R₃ : γ → δ → Prop) : (fun a d => ∃ c, (fun a c => ∃ b, R₁ a b ∧ R₂ b c) a c ∧ R₃ c d) = (fun a d => ∃ b, R₁ a b ∧ (fun b d => ∃ c, R₂ b c ∧ R₃ c d) b d) := by sorrySource