image_coe_Ici

Mathlib.Order.Interval.Set.WithBotTop

URI: https://scilib.ai/kg/mathlib#WithBot.image_coe_Ici

← MathLib Explorer

English

The image of Ici(a) under φ equals Ici(â).

Русский

Образ Ici(a) при вложении φ равен Ici(â).

LaTeX

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

Lean4

theorem image_coe_Ici : (some : α → WithBot α) '' Ici a = Ici (a : WithBot α) := by
  rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru