English
If e is a rel-iso from r to s, then the image of a max chain under e is a max chain.
Русский
Если e — отображение-реляционный из r в s, то образ максимальной цепи под e является максимальной цепью.
LaTeX
$$$ IsMaxChain\\ r\\ c \\rightarrow IsMaxChain\\ s\\ (e '' c) $$$
Lean4
theorem image {s : β → β → Prop} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) : IsMaxChain s (e '' c)
where
left := hc.isChain.image _ _ _ fun _ _ ↦ by exact e.map_rel_iff.2
right t ht
hf := by
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, preimage_equiv_eq_image_symm]
exact hc.2 (ht.image _ _ _ fun _ _ ↦ by exact e.symm.map_rel_iff.2) ((e.toEquiv.subset_symm_image _ _).2 hf)
