Ioo_succ_right_eq_insert_of_not_isMax

English

If a < b and b is not maximal, then Ioo(a, succ(b)) equals insert b Ioo(a,b).

Русский

Если a < b и b не максимален, то Ioo(a, succ(b)) = insert b Ioo(a,b).

LaTeX

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

Lean4

theorem Ioo_succ_right_eq_insert_of_not_isMax (h₁ : a < b) (h₂ : ¬IsMax b) : Ioo a (succ b) = insert b (Ioo a b) := by
  simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

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