image_coe_Ioi — Mathlib

English

The image of Ioi a under φ is Ioi â, i.e., φ(Ioi(a)) = Ioi(φ(a)).

Русский

Образ Ioi a при вложении φ равен Ioi â, то есть φ(Ioi(a)) = Ioi(φ(a)).

LaTeX

$$$ \phi(\mathrm{Ioi}(a)) = \mathrm{Ioi}(\hat{a}). $$$

Lean4

theorem image_coe_Ioi : (some : α → WithBot α) '' Ioi a = Ioi (a : WithBot α) := by
  rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]

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