insert_Ico_pred_right_eq_Ico — Mathlib

English

Let a < b in a linearly ordered set with LocallyFiniteOrder and PredOrder. Inserting pred(b) into Ico(a, pred(b)) gives Ico(a, b).

Русский

Пусть a < b в линейном порядке с локально конечным порядком и предшественником. Добавление pred(b) в Ico(a, pred(b)) даёт Ico(a, b).

LaTeX

$$$ \{\operatorname{pred}(b)\} \cup Ico(a, \operatorname{pred}(b)) = Ico(a,b)$$$

Lean4

theorem insert_Ico_pred_right_eq_Ico (h : a < b) : insert (pred b) (Ico a (pred b)) = Ico a b :=
  coe_injective <| by simpa using Set.insert_Ico_pred_right_eq_Ico h

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