image_Ioi — Mathlib

English

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

Русский

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

LaTeX

$$$$ e'' Ioi(a) = Ioi(e(a)) $$$$

Lean4

@[simp]
theorem image_Ioi (e : α ≃o β) (a : α) : e '' Ioi a = Ioi (e a) :=
  e.dual.image_Iio a

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