English
Relation lifting through map: if R ⇒ P holds between elements, then map respects Forall₂, i.e., mapping both lists preserves the P-relationship along Forall₂.
Русский
Отображение через map сохраняет отношение: если R ⇒ P между элементами, то отображение списков сохраняет связь P через Forall₂.
LaTeX
$$$ \mathrm{rel\_map} : ((R \Rightarrow P) \Rightarrow \mathrm{Forall₂}\ R \Rightarrow \mathrm{Forall₂}\ P)\ \mathrm{map}\ \mathrm{map}$$$
Lean4
theorem rel_map : ((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map map
| _, _, _, [], [], Forall₂.nil => Forall₂.nil
| _, _, h, _ :: _, _ :: _, Forall₂.cons h₁ h₂ => Forall₂.cons (h h₁) (rel_map (@h) h₂)
