insert_Ioc_left_eq_Ioc_pred_of_not_isMin

English

Let a ≤ b in a linearly ordered set with LocallyFiniteOrder and PredOrder. If a is not the minimum, then the set obtained by inserting a into Ioc(a,b) is equal to Ioc(pred a, b).

Русский

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

LaTeX

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

Lean4

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

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