English
If S is a binary relation on β and f : α → β, and there is a compatibility map H that translates S into R via f (i.e., S(f a, f b) implies R a b), then whenever map f l is an S-chain, l is an R-chain.
Русский
Пусть S — отношение на β, f : α → β, и пусть существует отображение H: для любых a,b в α, S(f a, f b) ⇒ R a b. Тогда если список map f l образует S-цепь, то l образует R-цепь.
LaTeX
$$$IsChain\\ S(\\mathrm{map}\\ f\\ l) \\Rightarrow (\\forall a\\, b\\, ha\\, hb,\\; S( f\\ a\\ ha) (f\\ b\\ hb) \\Rightarrow R\\ a\\ b) \\Rightarrow IsChain\\ R\\ l$$$
Lean4
theorem isChain_of_isChain_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b) {l : List α}
(p : IsChain S (map f l)) : IsChain R l :=
((isChain_map f).1 p).imp H
