Ioo_pred_left_eq_Ioc_of_not_isMin

English

Let α be a linearly ordered set with a predecessor. If a is not the minimum, then for every b the open interval from pred(a) to b equals the half-open interval from a to b, i.e. Ioo(pred a, b) = Ico(a, b).

Русский

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

LaTeX

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

Lean4

theorem Ioo_pred_left_eq_Ioc_of_not_isMin (ha : ¬IsMin a) (b : α) : Ioo (pred a) b = Ico a b := by ext x;
  rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]

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