English
Let M and N be preordered sets and f an order isomorphism between them; if N is locally finite, then M inherits a LocallyFiniteOrder structure by transporting the finitary interval structure along f: define finsetIccM(x,y) to be the image under f^{-1} of finsetIccN(fx,fy), and similarly for finsetIco, finsetIoc, finsetIoo.
Русский
Пусть M и N — предпорядки, а f — это упорядоченная изоморфия между ними; если N удовлетворяет условию локальной конечности, то M наследует структуру LocallyFiniteOrder путём переноса структуры конечных интервалов вдоль f: задаём finsetIccM(x,y) как образ через f^{-1} от finsetIccN(fx,fy), аналогично для finsetIco, finsetIoc, finsetIoo.
LaTeX
$$$\text{DenselyFiniteOrderTransfer} =\;\text{finsetIcc}_M(x,y) = \operatorname{map}_{f^{-1}}(\operatorname{finsetIcc}_N(fx,fy)) ,\; \text{and similarly for } \operatorname{finsetIco}, \operatorname{finsetIoc}, \operatorname{finsetIoo}.\; M \text{ is LocallyFiniteOrder.}$$$
Lean4
/-- A `LocallyFiniteOrder` can be transferred across an order isomorphism. -/
-- See note [reducible non-instances]
abbrev ofOrderIsoClass {F M N : Type*} [Preorder M] [Preorder N] [EquivLike F M N] [OrderIsoClass F M N] (f : F)
[LocallyFiniteOrder N] : LocallyFiniteOrder M
where
finsetIcc x y := (finsetIcc (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
finsetIco x y := (finsetIco (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
finsetIoc x y := (finsetIoc (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
finsetIoo x y := (finsetIoo (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
finset_mem_Icc := by simp [finset_mem_Icc, EquivLike.inv_apply_eq]
finset_mem_Ico := by simp [finset_mem_Ico, EquivLike.inv_apply_eq, map_lt_map_iff]
finset_mem_Ioc := by simp [finset_mem_Ioc, EquivLike.inv_apply_eq, map_lt_map_iff]
finset_mem_Ioo := by simp [finset_mem_Ioo, EquivLike.inv_apply_eq, map_lt_map_iff]
