English
Let R be a relation on α, β and S a relation on γ, δ. If s1 and s2 are LiftRel R, and whenever a relation holds between a and b, it implies S between f1 a and f2 b, then the maps map f1 s1 and map f2 s2 are related by LiftRel S.
Русский
Пусть R — отношение между α и β, а S — отношение между γ и δ. Если s1 и s2 удовлетворяют LiftRel R, и когда существует связь между a и b, тогда между f1 a и f2 b следует S, то отображения map f1 s1 и map f2 s2 удовлетворяют LiftRel S.
LaTeX
$$$\text{LiftRel } R\; s_1\; s_2 \rightarrow \big(\forall a,b,\; R\ a\ b \rightarrow S\ (f_1\ a) (f_2\ b)\big) \Rightarrow \mathrm{LiftRel}\ S\ (\mathrm{map}\ f_1\ s_1) (\mathrm{map}\ f_2\ s_2)$$$
Lean4
theorem liftRel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : WSeq α} {s2 : WSeq β} {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) :=
⟨fun s1 s2 => ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t, ⟨s1, s2, rfl, rfl, h1⟩, fun {s1 s2} h =>
match s1, s2, h with
| _, _, ⟨s, t, rfl, rfl, h⟩ => by
simp only [exists_and_left, destruct_map]
apply Computation.liftRel_map _ _ (liftRel_destruct h)
intro o p h
rcases o with - | a <;> rcases p with - | b
· simp
· cases b; cases h
· cases a; cases h
· obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
obtain ⟨r, h⟩ := h
exact ⟨h2 r, s, rfl, t, rfl, h⟩⟩
