image_Ioo — Mathlib

English

If e is an order-embedding and range e is OrdConnected, then e''Ioo x y = Ioo(e x) (e y).

Русский

Если e — вложение в порядок и диапазон e OrdConnected, то образ Ioo x y равен Ioo (e x) (e y).

LaTeX

$$$e''\mathrm{Ioo}(x,y) = \mathrm{Ioo}(e(x), e(y)).$$$

Lean4

theorem image_Ioo (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Ioo x y = Ioo (e x) (e y) := by
  rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

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