insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin

English

If a ≤ b and a is not a minimum, then inserting a into Ioc a b yields Ioc(a-1) b: insert a (Ioc a b) = Ioc(a-1) b.

Русский

Пусть a ≤ b и a не минимален. Тогда вставка a в Ioc a b даёт Ioc(a-1) b: insert a (Ioc a b) = Ioc(a-1) b.

LaTeX

$$$a \le b \Rightarrow \lnot IsMin(a) \Rightarrow Ioc(a,b) \cup \{a\} = Ioc(a-1,b)$$$

Lean4

theorem insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin (h : a ≤ b) (ha : ¬IsMin a) : insert a (Ioc a b) = Ioc (a - 1) b :=
  by simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred_of_not_isMin h ha

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