preimage_coe_Ico

Mathlib.Order.Interval.Set.WithBotTop

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

English

The embedding preserves half-open intervals: φ^{-1}(Ico(a,b)) = Ico(a,b) for all a,b.

Русский

Встраивание сохраняет полуоткрытые интервалы: φ^{-1}(Ico(a,b)) = Ico(a,b) для всех a,b.

LaTeX

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

Lean4

@[simp]
theorem preimage_coe_Ico : (some : α → WithBot α) ⁻¹' Ico a b = Ico a b := by simp [← Ici_inter_Iio]

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

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

Разделы

Аффилиация

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