English
Let s be a chain with respect to a relation r, and φ be a relational isomorphism from r to r'. Then the image φ''s is a chain with respect to r'.
Русский
Пусть s является цепью относительно отношения r, а φ — отношение-изоморфизм от r к r'. Тогда образ φ''s является цепью относительно r'.
LaTeX
$$$ (IsChain\ r\ s \;\\wedge\\; \\phi : r \\simeq_r r') \\rightarrow IsChain\ r' (\\phi '' s) $$$
Lean4
theorem image_relIso (hs : IsChain r s) (φ : r ≃r r') : IsChain r' (φ '' s) :=
hs.image_relEmbedding φ.toRelEmbedding