preimage_coe_Ioc

Mathlib.Order.Interval.Set.WithBotTop

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

English

For all a,b, the preimage under φ of Ioc(a,b) equals Ioc(a,b).

Русский

Для всех a,b предобраз φ от Ioc(a,b) равен Ioc(a,b).

LaTeX

$$$ \forall a,b \in \alpha, \ \phi^{-1}(\mathrm{Ioc}(a,b)) = \mathrm{Ioc}(a,b). $$$

Lean4

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

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

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

Разделы

Аффилиация

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