Icc_succ_right — Mathlib

English

If a ≤ succ(b), then the closed interval [a, succ(b)] equals {succ(b)} union [a, b].

Русский

Если a ≤ succ(b), то пара Closed интервал [a, succ(b)] равен {succ(b)} ∪ [a, b].

LaTeX

$$$\text{If } a \leq \operatorname{succ} b:\; \mathrm{Icc}(a, \operatorname{succ} b) = \operatorname{insert}(\operatorname{succ} b)(\mathrm{Icc}(a, b))$$$

Lean4

theorem Icc_succ_right (h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b) := by
  simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]

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