image_Iio — Mathlib

English

Let e be an order-embedding with range e an IsLowerSet. Then for every a, the image of the open lower ray Iio(a) under e equals Iio(e(a)): e'' Iio(a) = Iio(e(a)).

Русский

Пусть e — вложение порядка с диапазоном, образующим нижнее множество. Тогда для каждого a выполняется e'' Iio(a) = Iio(e(a)).

LaTeX

$$$e'' Iio(a) = Iio(e(a))$$$

Lean4

theorem image_Iio (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) : e '' Iio a = Iio (e a) :=
  e.dual.image_Ioi he a

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