English
Mapping the elements of a cycle by a function f preserves chain structure up to the induced relation on the target.
Русский
Отображение элементов цикла функцией f сохраняет структуру цепи в целевой области по отношению, заданному на целевой области.
LaTeX
$$$$ Chain\\ r\\ (Cycle.map\\ f\\ s) \\iff Chain\\ (\\lambda a b, r\\ (f\\ a) (f\\ b))\\ s. $$$$
Lean4
theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} :
Chain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s :=
Quotient.inductionOn s fun l => by
rcases l with - | ⟨a, l⟩
· rfl
· simp [← concat_eq_append, ← map_concat, List.isChain_cons_map f]
