image_Ioo — Mathlib

English

Let e be an order isomorphism between α and β. Then the image of the open interval Ioo(a,b) under e is the open interval Ioo(e(a), e(b)); i.e., e''Ioo(a,b) = Ioo(e(a), e(b)).

Русский

Пусть e — изоморфизм порядка между α и β. Тогда образ открытого интервала Ioo(a,b) равен Ioo(e(a), e(b)).

LaTeX

$$$$ e'' Ioo(a,b) = Ioo(e(a), e(b)) $$$$

Lean4

@[simp]
theorem image_Ioo (e : α ≃o β) (a b : α) : e '' Ioo a b = Ioo (e a) (e b) := by
  rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]

Похожие утверждения