insert_Ico_left_eq_Ico_pred_of_not_isMin

English

Let a ≤ b in a linearly ordered set with LocallyFiniteOrder and PredOrder. If a is not the minimum, then inserting pred(a) into Ico(a,b) yields Ico(pred(a), b).

Русский

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

LaTeX

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

Lean4

theorem insert_Ico_left_eq_Ico_pred_of_not_isMin (h : a ≤ b) (ha : ¬IsMin a) :
    insert (pred a) (Ico a b) = Ico (pred a) b :=
  coe_injective <| by simpa using Set.insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

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