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