Theorems · Theorem · order theory

RelSeries.append_assoc

∀ {α : Type u_1} {r : SetRel α α} (p q w : RelSeries r) (hpq : (p.last, q.head) ∈ r) (hqw : (q.last, w.head) ∈ r),
  (p.append q hpq).append w ⋯ = p.append (q.append w hqw) ⋯

Defined in

Mathlib.Order.RelSeries

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound