English
Transport LocallyFiniteOrderTop across an OrderIso: the finsetIci and finsetIoi on α correspond to the image of Ici and Ioi in β under f, with finset_mem_Ici and finset_mem_Ioi preserved.
Русский
Перенос локально конечно упорядоченного верхнего элемента через порядок-изоморфизм: finsetIci и finsetIoi на α соответствуют образам Ici и Ioi в β через f, сохранены условия принадлежности.
LaTeX
$$$$ \\bigl( \\mathrm{locallyFiniteOrderTop}\\ α \\bigr) = \\cdots \\quad\\text{(перенос через } f \\text{)} $$$$
Lean4
/-- Transfer `LocallyFiniteOrderTop` across an `OrderIso`. -/
abbrev locallyFiniteOrderTop [LocallyFiniteOrderTop β] (f : α ≃o β) : LocallyFiniteOrderTop α
where
finsetIci a := (Ici (f a)).map f.symm.toEquiv.toEmbedding
finsetIoi a := (Ioi (f a)).map f.symm.toEquiv.toEmbedding
finset_mem_Ici := by simp
finset_mem_Ioi := by
simp
-- See note [reducible non-instances]
