English
Let f be an order isomorphism between preordered types α and β, and suppose β has LocallyFiniteOrder. Then α inherits LocallyFiniteOrder by transporting all interval finsets along f: finsetIcc a b = map f.symm toEquiv toEmbedding (Icc f a f b), finsetIco a b = map f.symm toEquiv toEmbedding (Ico f a f b), etc., and the corresponding membership properties hold.
Русский
Пусть f — перестановка по порядку между упорядоченными множностями α и β, и β обладает свойством локальной конечности интервалов. Тогда α наследует это свойство, переводом всех конечных множеств интервалов вдоль f: finsetIcc a b = map f.symm ... (Icc f a f b) и т.д., а соответствующие свойства принадлежности сохраняются.
LaTeX
$$$$ \\text{[LocallyFiniteOrder transported along } f: α \\simeq_{o} β \\text{]} \\\\ \\mathrm{finsetIcc}\ a\ b = (\\mathrm{Icc}\\ (f\\ a)\\ (f\\ b)).\\mathrm{map}\\, f^{-1}_{\\mathrm{equiv}} \\mathrm{toEmbedding}, \\text{ etc.} $$$$
Lean4
/-- Transfer `LocallyFiniteOrder` across an `OrderIso`. -/
abbrev locallyFiniteOrder [LocallyFiniteOrder β] (f : α ≃o β) : LocallyFiniteOrder α
where
finsetIcc a b := (Icc (f a) (f b)).map f.symm.toEquiv.toEmbedding
finsetIco a b := (Ico (f a) (f b)).map f.symm.toEquiv.toEmbedding
finsetIoc a b := (Ioc (f a) (f b)).map f.symm.toEquiv.toEmbedding
finsetIoo a b := (Ioo (f a) (f b)).map f.symm.toEquiv.toEmbedding
finset_mem_Icc := by simp
finset_mem_Ico := by simp
finset_mem_Ioc := by simp
finset_mem_Ioo := by
simp
-- See note [reducible non-instances]
