image_Icc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_Icc (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) : e '' Icc x y = Icc (e x) (e y) := by
  rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

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