image_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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