English
Let e be an order isomorphism between α and β. Then the image of the closed interval Icc(a,b) under e is Icc(e(a), e(b)); i.e., e''Icc(a,b) = Icc(e(a), e(b)).
Русский
Пусть e — изоморфизм порядка между α и β. Тогда образ замкнутого интервала Icc(a,b) равен Icc(e(a), e(b)).
LaTeX
$$$$ e'' Icc(a,b) = Icc(e(a), e(b)) $$$$
Lean4
@[simp]
theorem image_Icc (e : α ≃o β) (a b : α) : e '' Icc a b = Icc (e a) (e b) := by
rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]