Relation_Composition_Associativity_Pointwise
ProvedRelation composition is associative at each point: (R₃ ∘ R₂) ∘ R₁ and R₃ ∘ (R₂ ∘ R₁) agree element-wise.
Preamble
import Mathlib.Tactic
Formal statement
theorem Relation_Composition_Associativity_Pointwise {α β γ δ : Type _} (R₁ : α → β → Prop) (R₂ : β → γ → Prop) (R₃ : γ → δ → Prop) (a : α) (d : δ) : (∃ c, (∃ b, R₁ a b ∧ R₂ b c) ∧ R₃ c d) ↔ (∃ b, R₁ a b ∧ (∃ c, R₂ b c ∧ R₃ c d)) := by sorry