image_Ici — Mathlib

English

If e is an order-embedding and the range of e is upper, then the image of Ici a under e is Ici at e(a).

Русский

Если e — вложение порядка и образ e является верхним, тогда образ Ici a под действием e равен Ici (e a).

LaTeX

$$$\\forall a, e''(Ici(a)) = Ici(e(a))$ (under the given hypothesis about range e)$$

Lean4

theorem image_Ici (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) : e '' Ici a = Ici (e a) := by
  rw [← e.preimage_Ici, image_preimage_eq_inter_range, inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

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