Ioc_pred_right

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Ioc_pred_right

English

Ioc a (pred b) = Ioo a b.

Русский

Ioc a pred b = Ioo a b.

LaTeX

$$$$Ioc(a, pred(b)) = Ioo(a,b).$$$$

Lean4

@[simp]
theorem Ioc_pred_right (a b : α) : Ioc a (pred b) = Ioo a b :=
  Ioc_pred_right_of_not_isMin <| not_isMin _

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

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

Разделы

Аффилиация

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