preimage_coe_Ioc_bot

Mathlib.Order.Interval.Set.WithBotTop

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

English

The preimage of Ioc(⊥,a) under φ equals Iic(a).

Русский

Предобраз φ от Ioc(⊥,a) равен Iic(a).

LaTeX

$$$ \phi^{-1}(\mathrm{Ioc}(\bot,a)) = \mathrm{Iic}(a). $$$

Lean4

@[simp]
theorem preimage_coe_Ioc_bot : (some : α → WithBot α) ⁻¹' Ioc ⊥ a = Iic a := by simp [← Ioi_inter_Iic]

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

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

Разделы

Аффилиация

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