image_coe_Iio

Mathlib.Order.Interval.Set.WithBotTop

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem image_coe_Iio : (some : α → WithTop α) '' Iio a = Iio (a : WithTop α) := by
  rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]

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

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

Разделы

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

Аффилиация

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