English
Let e be an order-embedding between preordered sets, and suppose the range of e is an upper set. Then for every a, the image of the open upper ray Ioi(a) under e equals the upper ray of e(a): e'' Ioi(a) = Ioi(e(a)).
Русский
Пусть e — вложение порядка между частично упорядоченными множествами и область значений e образует верхнее множество. Тогда для всякого a выполняется равенство образа множества {x | a < x} через e равному {y | e(a) < y}.
LaTeX
$$$e'' Ioi(a) = Ioi(e(a))$$$
Lean4
theorem image_Ioi (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) : e '' Ioi a = Ioi (e a) := by
rw [← e.preimage_Ioi, image_preimage_eq_inter_range, inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]
