image_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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