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