image_coe_Iic

Mathlib.Order.Interval.Set.WithBotTop

URI: https://scilib.ai/kg/mathlib#WithTop.image_coe_Iic

← MathLib Explorer

English

The image of Iic(a) under i is the interval Iic(i(a)) in WithTop α.

Русский

Образ Iic(a) под i — это интервал Iic(i(a)) в WithTop α.

LaTeX

$$$$ i''(\mathrm{Iic}(a)) = \mathrm{Iic}(\mathrm{i}(a)) $$$$

Lean4

theorem image_coe_Iic : (some : α → WithTop α) '' Iic a = Iic (a : WithTop α) := by
  rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]

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

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

Разделы

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

Аффилиация

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