Ici_succ_eq_Ioi_of_not_isMax — Mathlib

English

If a is not maximal, the right-closed interval starting at succ(a) coincides with the right open interval from a: Ici(succ a) = Ioi a.

Русский

Если a не максимум, правая полузакрытая интервал от succ(a) совпадает с правой открытой от a: Ici(succ a) = Ioi a.

LaTeX

$$$ Ici(\operatorname{succ}(a)) = Ioi(a) $$$

Lean4

theorem Ici_succ_eq_Ioi_of_not_isMax (ha : ¬IsMax a) : Ici (succ a) = Ioi a :=
  coe_injective <| by simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

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