insert_Ioc_left_eq_Ioc_sub_one — Mathlib

English

In the discrete order, inserting b into Ioc(a,b) yields Ioc(a,b) with the right boundary extended by 1: Ioc(a,b) ∪ {b} = Ioc(a,b+1).

Русский

В дискретном порядке вставка b в Ioc(a,b) расширяет правую границу на 1: Ioc(a,b) ∪ {b} = Ioc(a,b+1).

LaTeX

$$$ \mathrm{Ioc}(a,b) \cup \{b\} = \mathrm{Ioc}(a,b+1) $$$

Lean4

theorem insert_Ioc_left_eq_Ioc_sub_one (h : a ≤ b) : insert a (Ioc a b) = Ioc (a - 1) b := by
  simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred h

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