Ioc_succ_right — Mathlib

English

If a < succ(b), then Ioc(a, succ(b)) equals {succ(b)} union Ioc(a, b).

Русский

Если a < succ(b), то Ioc(a, succ(b)) равно {succ(b)} ∪ Ioc(a, b).

LaTeX

$$$\,a < \operatorname{succ} b \Rightarrow \mathrm{Ioc}(a, \operatorname{succ} b) = \operatorname{insert}(\operatorname{succ} b)(\mathrm{Ioc}(a, b))$$$

Lean4

theorem Ioc_succ_right (h : a < succ b) : Ioc a (succ b) = insert (succ b) (Ioc a b) := by
  simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]

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