English
Transport LocallyFiniteOrderBot across an OrderIso: the finsetIic and finsetIio on α correspond to the image of Iic and Iio in β under f, with finset_mem_Iic and finset_mem_Iio preserved.
Русский
Перенос локально конечного нижнего порядка через порядок-изоморфизм: finsetIic и finsetIio на α соответствуют образам Iic и Iio в β через f, сохранены условия принадлежности.
LaTeX
$$$$ \\bigl( \\mathrm{locallyFiniteOrderBot}\\ α \\bigr) = \\cdots $$$$
Lean4
/-- Transfer `LocallyFiniteOrderBot` across an `OrderIso`. -/
abbrev locallyFiniteOrderBot [LocallyFiniteOrderBot β] (f : α ≃o β) : LocallyFiniteOrderBot α
where
finsetIic a := (Iic (f a)).map f.symm.toEquiv.toEmbedding
finsetIio a := (Iio (f a)).map f.symm.toEquiv.toEmbedding
finset_mem_Iic := by simp
finset_mem_Iio := by simp
