Iio_succ_eq_Iic_of_not_isMax — Mathlib

English

If b is not a maximum, then the open interval below succ(b) equals the closed interval at b: Iio(succ(b)) = Iic(b).

Русский

Если b не максимум, тогда открытый интервал слева от succ(b) равен закрытому интервалу в b: Iio(succ(b)) = Iic(b).

LaTeX

$$$ Iio(\operatorname{succ}(b)) = Iic(b) $$$

Lean4

theorem Iio_succ_eq_Iic_of_not_isMax (hb : ¬IsMax b) : Iio (succ b) = Iic b :=
  coe_injective <| by simpa using Set.Iio_succ_eq_Iic_of_not_isMax hb

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