English
If LiftRel R s1 s2 and maps f1,f2 preserve R to S, then LiftRel S (map f1 s1) (map f2 s2).
Русский
Если LiftRel R s1 s2 и отображения f1, f2 сохраняют связь через R в S, то LiftRel S (map f1 s1) (map f2 s2).
LaTeX
$$$\\mathrm{LiftRel}\\,R\\ s1\\ s2 \\Rightarrow\\ (\\forall {a b}, R\\ a\\ b \\rightarrow \\mathrm{LiftRel}\\,S (f1\\ a) (f2\\ b)) \\Rightarrow \\mathrm{LiftRel}\\,S (\\mathrm{map}\\ f1\\ s1) (\\mathrm{map}\\ f2\\ s2)$$$
Lean4
theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α} {s2 : Computation β} {f1 : α → γ}
{f2 : β → δ} (h1 : LiftRel R s1 s2) (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b)) : LiftRel S (map f1 s1) (map f2 s2) :=
by rw [← bind_pure, ← bind_pure]; apply liftRel_bind _ _ h1; simpa
