English
If r is transitive, and Rel r s t and Rel r t u hold, then Rel r s u holds.
Русский
Если r транзитивно, и Rel r s t и Rel r t u верны, то Rel r s u верно.
LaTeX
$$$Rel\ r\ s\ t \to Rel\ r\ t\ u \to Rel\ r\ s\ u$$$
Lean4
protected nonrec theorem trans (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u) :
Rel r s u := by
induction t using Multiset.induction_on generalizing s u with
| empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
| cons x t ih =>
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)
