Ioc_pred_pred_eq_Ico_of_not_isMin

English

Let α be a linearly ordered set with a predecessor. If a is not the minimum, then for every b, Ioc(pred(a), pred(b)) = Ico(a, b).

Русский

Пусть α — линейно упорядочено с предшественником. Пусть a не минимален. Тогда для любого b выполняется Ioc(pred(a), pred(b)) = Ico(a, b).

LaTeX

$$$Ioc(\operatorname{pred} a, \operatorname{pred} b) = Ico(a, b)$$$

Lean4

theorem Ioc_pred_pred_eq_Ico_of_not_isMin (ha : ¬IsMin a) (b : α) : Ioc (pred a) (pred b) = Ico a b := by
  rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]

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