English
An order isomorphism e: α ≃o β between lattices induces an order isomorphism between the closed-intervals Icc x y and Icc (e x) (e y) for all x, y ∈ α.
Русский
Изоморфизм порядка e: α ≃o β между решетками индуцирует изоморфизм между замкнутыми интервалами Icc x y и Icc (e x) (e y) для любых x, y ∈ α.
LaTeX
$$$Icc(x,y) \cong_o Icc(e(x),e(y))$$$
Lean4
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices. -/
protected def Icc [Lattice α] [Lattice β] (e : α ≃o β) (x y : α) : Icc x y ≃o Icc (e x) (e y)
where
toFun z := ⟨e z, by simp only [mem_Icc, map_le_map_iff]; exact z.property⟩
invFun z := ⟨e.symm z, by simp only [mem_Icc, e.le_symm_apply, e.symm_apply_le]; exact z.property⟩
left_inv y := by simp
right_inv y := by simp
map_rel_iff' := by simp
