English
Let R be a transitive relation on α. If s is LiftRel-related to t and t is LiftRel-related to u, then s is LiftRel-related to u.
Русский
Пусть R — транситивное отношение на α. Если вычисления s и t связаны LiftRel R, а t и u связаны LiftRel R, то s и u связаны LiftRel R.
LaTeX
$$$\\forall \\alpha\\, (R:\\alpha \\to \\alpha \\to \\mathrm{Prop}),\\ \\mathrm{Transitive}~R \\Rightarrow \\mathrm{Transitive}(\\mathrm{LiftRel}\\,R)$$$
Lean4
theorem trans (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R) := fun _ _ _ ⟨l1, r1⟩ ⟨l2, r2⟩ =>
⟨fun {_} a1 =>
let ⟨_, b2, ab⟩ := l1 a1
let ⟨c, c3, bc⟩ := l2 b2
⟨c, c3, H ab bc⟩,
fun {_} c3 =>
let ⟨_, b2, bc⟩ := r2 c3
let ⟨a, a1, ab⟩ := r1 b2
⟨a, a1, H ab bc⟩⟩
