English
The lifted relation is transitive if the base relation is transitive.
Русский
Поднятое отношение транзитивно, если базовое отношение транзитивно.
LaTeX
$$$$ \mathrm{Transitive}(R) \Rightarrow \mathrm{Transitive}(\mathrm{LiftRel}\ R). $$$$
Lean4
theorem trans (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R) := fun s t u h1 h2 =>
by
refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
rcases h with ⟨t, h1, h2⟩
have h1 := liftRel_destruct h1
have h2 := liftRel_destruct h2
refine
Computation.liftRel_def.2
⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2), fun {a c} ha hc => ?_⟩
rcases h1.left ha with ⟨b, hb, t1⟩
have t2 := Computation.rel_of_liftRel h2 hb hc
obtain - | a := a <;> obtain - | c := c
· trivial
· cases b
· cases t2
· cases t1
· cases a
rcases b with - | b
· cases t1
· cases b
cases t2
· obtain ⟨a, s⟩ := a
rcases b with - | b
· cases t1
obtain ⟨b, t⟩ := b
obtain ⟨c, u⟩ := c
obtain ⟨ab, st⟩ := t1
obtain ⟨bc, tu⟩ := t2
exact ⟨H ab bc, t, st, tu⟩
