English
Let R be a binary relation on α and f a function β → α. For every list l of β, l is an R-chain after applying f if and only if l is a chain with respect to the relation on β defined by S(a,b) := R(f(a), f(b)).
Русский
Пусть R — двоичное отношение на множество α, а f : β → α. Для любого списка l из β выполняется: l является R-цепью после применения f тогда и только тогда, когда l является цепью относительно отношения S на β, где S(a,b) = R(f(a), f(b)).
LaTeX
$$$IsChain\\ R(\\mathrm{map}\\ f\\ l) \\iff IsChain(\\lambda a\\, b.\\, R(f\\,a)\\, (f\\,b))\\ l$$$
Lean4
theorem isChain_map (f : β → α) {l : List β} : IsChain R (map f l) ↔ IsChain (fun a b : β => R (f a) (f b)) l := by
induction l using twoStepInduction <;> grind
