insert_Ioc_right_eq_Ioc_succ — Mathlib

English

For a linearly ordered locally finite successor-order, inserting succ(b) into Ico a b yields Ico a (succ b).

Русский

Для линейного локально конечного порядка с succ, вставка succ(b) в Ico a b даёт Ico a (succ(b)).

LaTeX

$$$\forall a,b:\, α,\ (\mathrm{le}\ a b) \Rightarrow \mathrm{insert}(\mathrm{succ}(b), \mathrm{Ico}(a,b)) = \mathrm{Ico}(a, \mathrm{succ}(b))$$$

Lean4

theorem insert_Ioc_right_eq_Ioc_succ (h : a ≤ b) : insert (succ b) (Ioc a b) = Ioc a (succ b) :=
  coe_injective <| by simpa using Set.insert_Ioc_right_eq_Ioc_succ h

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