image_coe_Icc — Mathlib

English

The image of Icc(a,b) under φ equals Icc(ā, b̂).

Русский

Образ Icc(a,b) при вложении φ равен Icc(ā, b̂).

LaTeX

$$$ \phi(\mathrm{Icc}(a,b)) = \mathrm{Icc}(\hat{a}, \hat{b}). $$$

Lean4

theorem image_coe_Icc : (some : α → WithBot α) '' Icc a b = Icc (a : WithBot α) b := by
  rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]

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