Ioc_pred_right_eq_Ioo

Mathlib.Order.Interval.Finset.SuccPred

URI: https://scilib.ai/kg/mathlib#Finset.Ioc_pred_right_eq_Ioo

English

In a linear locally finite order with PredOrder, Ioc a (pred b) equals Ioo a b.

Русский

В линейном локально конечном порядке с PredOrder: Ioc a (pred b) = Ioo a b.

LaTeX

$$$[PredOrder\ α] \Rightarrow Ioc(a, \mathrm{pred}(b)) = Ioo(a,b)$$$

Lean4

theorem Ioc_pred_right_eq_Ioo (a b : α) : Ioc a (pred b) = Ioo a b :=
  coe_injective <| by simpa using Set.Ioc_pred_right_eq_Ioo _ _

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

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

Разделы

Аффилиация

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