insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin

English

If a is not minimal, then inserting a into Ioc a b yields Ioc(a-1) b: Ioc(a,b) ∪ {a} = Ioc(a-1,b) with a ≤ b and a not minimal.

Русский

Если a не минимален, вставка a в Ioc(a,b) дает Ioc(a-1,b): Ioc(a,b) ∪ {a} = Ioc(a-1,b) при a ≤ b.

LaTeX

$$$ (a \le b) \land \neg \mathrm{IsMin}(a) \Rightarrow \mathrm{Ioc}(a,b) \cup \{a\} = \mathrm{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

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