Documentation

Mathlib.Order.Interval.Set.Basic

Intervals #

In any preorder, we define intervals (which on each side can be either infinite, open or closed) using the following naming conventions:

Each interval has the name I + letter for left side + letter for right side. For instance, Ioc a b denotes the interval (a, b]. The definitions can be found in Mathlib/Order/Interval/Set/Defs.lean.

This file contains basic facts on inclusion of and set operations on intervals (where the precise statements depend on the order's properties; statements requiring LinearOrder are in Mathlib/Order/Interval/Set/LinearOrder.lean).

TODO: This is just the beginning; a lot of rules are missing

instance Set.decidableMemIoo {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x x < b)] :
Decidable (x Ioo a b)
Equations
    instance Set.decidableMemIco {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a x x < b)] :
    Decidable (x Ico a b)
    Equations
      instance Set.decidableMemIio {α : Type u_1} [Preorder α] {b x : α} [Decidable (x < b)] :
      Equations
        instance Set.decidableMemIcc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a x x b)] :
        Decidable (x Icc a b)
        Equations
          instance Set.decidableMemIic {α : Type u_1} [Preorder α] {b x : α} [Decidable (x b)] :
          Equations
            instance Set.decidableMemIoc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x x b)] :
            Decidable (x Ioc a b)
            Equations
              instance Set.decidableMemIci {α : Type u_1} [Preorder α] {a x : α} [Decidable (a x)] :
              Equations
                instance Set.decidableMemIoi {α : Type u_1} [Preorder α] {a x : α} [Decidable (a < x)] :
                Equations
                  theorem Set.left_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} :
                  theorem Set.left_mem_Ico {α : Type u_1} [Preorder α] {a b : α} :
                  a Ico a b a < b
                  theorem Set.left_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :
                  a Icc a b a b
                  theorem Set.left_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} :
                  theorem Set.left_mem_Ici {α : Type u_1} [Preorder α] {a : α} :
                  a Ici a
                  theorem Set.right_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} :
                  theorem Set.right_mem_Ico {α : Type u_1} [Preorder α] {a b : α} :
                  theorem Set.right_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :
                  b Icc a b a b
                  theorem Set.right_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} :
                  b Ioc a b a < b
                  theorem Set.right_mem_Iic {α : Type u_1} [Preorder α] {a : α} :
                  a Iic a
                  @[simp]
                  theorem Set.Ici_toDual {α : Type u_1} [Preorder α] {a : α} :
                  @[deprecated Set.Ici_toDual (since := "2025-03-20")]
                  theorem Set.dual_Ici {α : Type u_1} [Preorder α] {a : α} :

                  Alias of Set.Ici_toDual.

                  @[simp]
                  theorem Set.Iic_toDual {α : Type u_1} [Preorder α] {a : α} :
                  @[deprecated Set.Iic_toDual (since := "2025-03-20")]
                  theorem Set.dual_Iic {α : Type u_1} [Preorder α] {a : α} :

                  Alias of Set.Iic_toDual.

                  @[simp]
                  theorem Set.Ioi_toDual {α : Type u_1} [Preorder α] {a : α} :
                  @[deprecated Set.Ioi_toDual (since := "2025-03-20")]
                  theorem Set.dual_Ioi {α : Type u_1} [Preorder α] {a : α} :

                  Alias of Set.Ioi_toDual.

                  @[simp]
                  theorem Set.Iio_toDual {α : Type u_1} [Preorder α] {a : α} :
                  @[deprecated Set.Iio_toDual (since := "2025-03-20")]
                  theorem Set.dual_Iio {α : Type u_1} [Preorder α] {a : α} :

                  Alias of Set.Iio_toDual.

                  @[simp]
                  theorem Set.Icc_toDual {α : Type u_1} [Preorder α] {a b : α} :
                  @[deprecated Set.Icc_toDual (since := "2025-03-20")]
                  theorem Set.dual_Icc {α : Type u_1} [Preorder α] {a b : α} :

                  Alias of Set.Icc_toDual.

                  @[simp]
                  theorem Set.Ioc_toDual {α : Type u_1} [Preorder α] {a b : α} :
                  @[deprecated Set.Ioc_toDual (since := "2025-03-20")]
                  theorem Set.dual_Ioc {α : Type u_1} [Preorder α] {a b : α} :

                  Alias of Set.Ioc_toDual.

                  @[simp]
                  theorem Set.Ico_toDual {α : Type u_1} [Preorder α] {a b : α} :
                  @[deprecated Set.Ico_toDual (since := "2025-03-20")]
                  theorem Set.dual_Ico {α : Type u_1} [Preorder α] {a b : α} :

                  Alias of Set.Ico_toDual.

                  @[simp]
                  theorem Set.Ioo_toDual {α : Type u_1} [Preorder α] {a b : α} :
                  @[deprecated Set.Ioo_toDual (since := "2025-03-20")]
                  theorem Set.dual_Ioo {α : Type u_1} [Preorder α] {a b : α} :

                  Alias of Set.Ioo_toDual.

                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem Set.nonempty_Icc {α : Type u_1} [Preorder α] {a b : α} :
                  (Icc a b).Nonempty a b
                  @[simp]
                  theorem Set.nonempty_Ico {α : Type u_1} [Preorder α] {a b : α} :
                  (Ico a b).Nonempty a < b
                  @[simp]
                  theorem Set.nonempty_Ioc {α : Type u_1} [Preorder α] {a b : α} :
                  (Ioc a b).Nonempty a < b
                  @[simp]
                  theorem Set.nonempty_Ici {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem Set.nonempty_Iic {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem Set.nonempty_Ioo {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] :
                  (Ioo a b).Nonempty a < b
                  @[simp]
                  theorem Set.nonempty_Ioi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
                  @[simp]
                  theorem Set.nonempty_Iio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
                  theorem Set.nonempty_Icc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a b) :
                  Nonempty (Icc a b)
                  theorem Set.nonempty_Ico_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
                  Nonempty (Ico a b)
                  theorem Set.nonempty_Ioc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
                  Nonempty (Ioc a b)
                  instance Set.nonempty_Ici_subtype {α : Type u_1} [Preorder α] {a : α} :
                  Nonempty (Ici a)

                  An interval Ici a is nonempty.

                  instance Set.nonempty_Iic_subtype {α : Type u_1} [Preorder α] {a : α} :
                  Nonempty (Iic a)

                  An interval Iic a is nonempty.

                  theorem Set.nonempty_Ioo_subtype {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] (h : a < b) :
                  Nonempty (Ioo a b)
                  instance Set.nonempty_Ioi_subtype {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
                  Nonempty (Ioi a)

                  In an order without maximal elements, the intervals Ioi are nonempty.

                  instance Set.nonempty_Iio_subtype {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
                  Nonempty (Iio a)

                  In an order without minimal elements, the intervals Iio are nonempty.

                  instance Set.instNoMinOrderElemIio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
                  instance Set.instNoMinOrderElemIic {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
                  instance Set.instNoMaxOrderElemIoi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
                  instance Set.instNoMaxOrderElemIci {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
                  @[simp]
                  theorem Set.Icc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a b) :
                  Icc a b =
                  @[simp]
                  theorem Set.Ico_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
                  Ico a b =
                  @[simp]
                  theorem Set.Ioc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
                  Ioc a b =
                  @[simp]
                  theorem Set.Ioo_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
                  Ioo a b =
                  @[simp]
                  theorem Set.Icc_eq_empty_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) :
                  Icc a b =
                  @[simp]
                  theorem Set.Ico_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b a) :
                  Ico a b =
                  @[simp]
                  theorem Set.Ioc_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b a) :
                  Ioc a b =
                  @[simp]
                  theorem Set.Ioo_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b a) :
                  Ioo a b =
                  theorem Set.Ico_self {α : Type u_1} [Preorder α] (a : α) :
                  Ico a a =
                  theorem Set.Ioc_self {α : Type u_1} [Preorder α] (a : α) :
                  Ioc a a =
                  theorem Set.Ioo_self {α : Type u_1} [Preorder α] (a : α) :
                  Ioo a a =
                  @[simp]
                  theorem Set.Ici_subset_Ici {α : Type u_1} [Preorder α] {a b : α} :
                  Ici a Ici b b a
                  theorem GCongr.Ici_subset_Ici_of_le {α : Type u_1} [Preorder α] {a b : α} :
                  b aSet.Ici a Set.Ici b

                  Alias of the reverse direction of Set.Ici_subset_Ici.

                  @[simp]
                  theorem Set.Ici_ssubset_Ici {α : Type u_1} [Preorder α] {a b : α} :
                  Ici a Ici b b < a
                  theorem GCongr.Ici_ssubset_Ici_of_le {α : Type u_1} [Preorder α] {a b : α} :
                  b < aSet.Ici a Set.Ici b

                  Alias of the reverse direction of Set.Ici_ssubset_Ici.

                  @[simp]
                  theorem Set.Iic_subset_Iic {α : Type u_1} [Preorder α] {a b : α} :
                  Iic a Iic b a b
                  theorem GCongr.Iic_subset_Iic_of_le {α : Type u_1} [Preorder α] {a b : α} :
                  a bSet.Iic a Set.Iic b

                  Alias of the reverse direction of Set.Iic_subset_Iic.

                  @[simp]
                  theorem Set.Iic_ssubset_Iic {α : Type u_1} [Preorder α] {a b : α} :
                  Iic a Iic b a < b
                  theorem GCongr.Iic_ssubset_Iic_of_le {α : Type u_1} [Preorder α] {a b : α} :
                  a < bSet.Iic a Set.Iic b

                  Alias of the reverse direction of Set.Iic_ssubset_Iic.

                  @[simp]
                  theorem Set.Ici_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} :
                  Ici a Ioi b b < a
                  @[simp]
                  theorem Set.Iic_subset_Iio {α : Type u_1} [Preorder α] {a b : α} :
                  Iic a Iio b a < b
                  theorem Set.Ioo_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
                  Ioo a₁ b₁ Ioo a₂ b₂
                  theorem Set.Ioo_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
                  Ioo a₂ b Ioo a₁ b
                  theorem Set.Ioo_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
                  Ioo a b₁ Ioo a b₂
                  theorem Set.Ico_subset_Ico {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
                  Ico a₁ b₁ Ico a₂ b₂
                  theorem Set.Ico_subset_Ico_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
                  Ico a₂ b Ico a₁ b
                  theorem Set.Ico_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
                  Ico a b₁ Ico a b₂
                  theorem Set.Icc_subset_Icc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
                  Icc a₁ b₁ Icc a₂ b₂
                  theorem Set.Icc_subset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
                  Icc a₂ b Icc a₁ b
                  theorem Set.Icc_subset_Icc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
                  Icc a b₁ Icc a b₂
                  theorem Set.Icc_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ < b₂) :
                  Icc a₁ b₁ Ioo a₂ b₂
                  theorem Set.Icc_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b Ici a
                  theorem Set.Icc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b Iic b
                  theorem Set.Ioc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b Iic b
                  theorem Set.Ioc_subset_Ioc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
                  Ioc a₁ b₁ Ioc a₂ b₂
                  theorem Set.Ioc_subset_Ioc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
                  Ioc a₂ b Ioc a₁ b
                  theorem Set.Ioc_subset_Ioc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
                  Ioc a b₁ Ioc a b₂
                  theorem Set.Ico_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h₁ : a₁ < a₂) :
                  Ico a₂ b Ioo a₁ b
                  theorem Set.Ioc_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
                  Ioc a b₁ Ioo a b₂
                  theorem Set.Icc_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h₁ : b₁ < b₂) :
                  Icc a b₁ Ico a b₂
                  theorem Set.Ioo_subset_Ico_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b Ico a b
                  theorem Set.Ioo_subset_Ioc_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b Ioc a b
                  theorem Set.Ico_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b Icc a b
                  theorem Set.Ioc_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b Icc a b
                  theorem Set.Ioo_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b Icc a b
                  theorem Set.Ico_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b Iio b
                  theorem Set.Ioo_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b Iio b
                  theorem Set.Ioc_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b Ioi a
                  theorem Set.Ioo_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b Ioi a
                  theorem Set.Ioi_subset_Ici_self {α : Type u_1} [Preorder α] {a : α} :
                  Ioi a Ici a
                  theorem Set.Iio_subset_Iic_self {α : Type u_1} [Preorder α] {a : α} :
                  Iio a Iic a
                  theorem Set.Ico_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b Ici a
                  theorem Set.Ioi_ssubset_Ici_self {α : Type u_1} [Preorder α] {a : α} :
                  Ioi a Ici a
                  theorem Set.Iio_ssubset_Iic_self {α : Type u_1} [Preorder α] {a : α} :
                  Iio a Iic a
                  theorem Set.Icc_subset_Icc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Icc a₂ b₂ a₂ a₁ b₁ b₂
                  theorem Set.Icc_subset_Ioo_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Ioo a₂ b₂ a₂ < a₁ b₁ < b₂
                  theorem Set.Icc_subset_Ico_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Ico a₂ b₂ a₂ a₁ b₁ < b₂
                  theorem Set.Icc_subset_Ioc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Ioc a₂ b₂ a₂ < a₁ b₁ b₂
                  theorem Set.Icc_subset_Iio_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Iio b₂ b₁ < b₂
                  theorem Set.Icc_subset_Ioi_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Ioi a₂ a₂ < a₁
                  theorem Set.Icc_subset_Iic_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Iic b₂ b₁ b₂
                  theorem Set.Icc_subset_Ici_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ b₁) :
                  Icc a₁ b₁ Ici a₂ a₂ a₁
                  theorem Set.Icc_ssubset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ b₂) (ha : a₂ < a₁) (hb : b₁ b₂) :
                  Icc a₁ b₁ Icc a₂ b₂
                  theorem Set.Icc_ssubset_Icc_right {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ b₂) (ha : a₂ a₁) (hb : b₁ < b₂) :
                  Icc a₁ b₁ Icc a₂ b₂
                  theorem Set.Ioi_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : a b) :
                  Ioi b Ioi a

                  If a ≤ b, then (b, +∞) ⊆ (a, +∞). In preorders, this is just an implication. If you need the equivalence in linear orders, use Ioi_subset_Ioi_iff.

                  theorem Set.Ioi_ssubset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
                  Ioi b Ioi a

                  If a < b, then (b, +∞) ⊂ (a, +∞). In preorders, this is just an implication. If you need the equivalence in linear orders, use Ioi_ssubset_Ioi_iff.

                  theorem Set.Ioi_subset_Ici {α : Type u_1} [Preorder α] {a b : α} (h : a b) :
                  Ioi b Ici a

                  If a ≤ b, then (b, +∞) ⊆ [a, +∞). In preorders, this is just an implication. If you need the equivalence in dense linear orders, use Ioi_subset_Ici_iff.

                  theorem Set.Iio_subset_Iio {α : Type u_1} [Preorder α] {a b : α} (h : a b) :
                  Iio a Iio b

                  If a ≤ b, then (-∞, a) ⊆ (-∞, b). In preorders, this is just an implication. If you need the equivalence in linear orders, use Iio_subset_Iio_iff.

                  theorem Set.Iio_ssubset_Iio {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
                  Iio a Iio b

                  If a < b, then (-∞, a) ⊂ (-∞, b). In preorders, this is just an implication. If you need the equivalence in linear orders, use Iio_ssubset_Iio_iff.

                  theorem Set.Iio_subset_Iic {α : Type u_1} [Preorder α] {a b : α} (h : a b) :
                  Iio a Iic b

                  If a ≤ b, then (-∞, a) ⊆ (-∞, b]. In preorders, this is just an implication. If you need the equivalence in dense linear orders, use Iio_subset_Iic_iff.

                  theorem Set.Ici_inter_Iic {α : Type u_1} [Preorder α] {a b : α} :
                  Ici a Iic b = Icc a b
                  theorem Set.Ici_inter_Iio {α : Type u_1} [Preorder α] {a b : α} :
                  Ici a Iio b = Ico a b
                  theorem Set.Ioi_inter_Iic {α : Type u_1} [Preorder α] {a b : α} :
                  Ioi a Iic b = Ioc a b
                  theorem Set.Ioi_inter_Iio {α : Type u_1} [Preorder α] {a b : α} :
                  Ioi a Iio b = Ioo a b
                  theorem Set.Iic_inter_Ici {α : Type u_1} [Preorder α] {a b : α} :
                  Iic a Ici b = Icc b a
                  theorem Set.Iio_inter_Ici {α : Type u_1} [Preorder α] {a b : α} :
                  Iio a Ici b = Ico b a
                  theorem Set.Iic_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} :
                  Iic a Ioi b = Ioc b a
                  theorem Set.Iio_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} :
                  Iio a Ioi b = Ioo b a
                  theorem Set.mem_Icc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x Ioo a b) :
                  x Icc a b
                  theorem Set.mem_Ico_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x Ioo a b) :
                  x Ico a b
                  theorem Set.mem_Ioc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x Ioo a b) :
                  x Ioc a b
                  theorem Set.mem_Icc_of_Ico {α : Type u_1} [Preorder α] {a b x : α} (h : x Ico a b) :
                  x Icc a b
                  theorem Set.mem_Icc_of_Ioc {α : Type u_1} [Preorder α] {a b x : α} (h : x Ioc a b) :
                  x Icc a b
                  theorem Set.mem_Ici_of_Ioi {α : Type u_1} [Preorder α] {a x : α} (h : x Ioi a) :
                  x Ici a
                  theorem Set.mem_Iic_of_Iio {α : Type u_1} [Preorder α] {a x : α} (h : x Iio a) :
                  x Iic a
                  theorem Set.Icc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b = ¬a b
                  theorem Set.Ico_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b = ¬a < b
                  theorem Set.Ioc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b = ¬a < b
                  theorem Set.Ioo_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] :
                  Ioo a b = ¬a < b
                  theorem IsTop.Iic_eq {α : Type u_1} [Preorder α] {a : α} (h : IsTop a) :
                  theorem IsBot.Ici_eq {α : Type u_1} [Preorder α] {a : α} (h : IsBot a) :
                  @[simp]
                  theorem Set.Ioi_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem Set.Iio_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem IsMax.Ioi_eq {α : Type u_1} [Preorder α] {a : α} :
                  IsMax aSet.Ioi a =

                  Alias of the reverse direction of Set.Ioi_eq_empty_iff.

                  @[simp]
                  theorem IsMin.Iio_eq {α : Type u_1} [Preorder α] {a : α} :
                  IsMin aSet.Iio a =

                  Alias of the reverse direction of Set.Iio_eq_empty_iff.

                  @[simp]
                  theorem Set.Iio_nonempty {α : Type u_1} [Preorder α] {a : α} :
                  @[simp]
                  theorem Set.Ioi_nonempty {α : Type u_1} [Preorder α] {a : α} :
                  theorem Set.Iic_inter_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (h : a c) :
                  Iic a Ioc b c = Ioc b a
                  theorem Set.notMem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
                  cIcc a b
                  @[deprecated Set.notMem_Icc_of_lt (since := "2025-05-23")]
                  theorem Set.not_mem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
                  cIcc a b

                  Alias of Set.notMem_Icc_of_lt.

                  theorem Set.notMem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
                  cIcc a b
                  @[deprecated Set.notMem_Icc_of_gt (since := "2025-05-23")]
                  theorem Set.not_mem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
                  cIcc a b

                  Alias of Set.notMem_Icc_of_gt.

                  theorem Set.notMem_Ico_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
                  cIco a b
                  @[deprecated Set.notMem_Ico_of_lt (since := "2025-05-23")]
                  theorem Set.not_mem_Ico_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
                  cIco a b

                  Alias of Set.notMem_Ico_of_lt.

                  theorem Set.notMem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
                  cIoc a b
                  @[deprecated Set.notMem_Ioc_of_gt (since := "2025-05-23")]
                  theorem Set.not_mem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
                  cIoc a b

                  Alias of Set.notMem_Ioc_of_gt.

                  theorem Set.notMem_Ioi_self {α : Type u_1} [Preorder α] {a : α} :
                  aIoi a
                  @[deprecated Set.notMem_Ioi_self (since := "2025-05-23")]
                  theorem Set.not_mem_Ioi_self {α : Type u_1} [Preorder α] {a : α} :
                  aIoi a

                  Alias of Set.notMem_Ioi_self.

                  theorem Set.notMem_Iio_self {α : Type u_1} [Preorder α] {b : α} :
                  bIio b
                  @[deprecated Set.notMem_Iio_self (since := "2025-05-23")]
                  theorem Set.not_mem_Iio_self {α : Type u_1} [Preorder α] {b : α} :
                  bIio b

                  Alias of Set.notMem_Iio_self.

                  theorem Set.notMem_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c a) :
                  cIoc a b
                  @[deprecated Set.notMem_Ioc_of_le (since := "2025-05-23")]
                  theorem Set.not_mem_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c a) :
                  cIoc a b

                  Alias of Set.notMem_Ioc_of_le.

                  theorem Set.notMem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b c) :
                  cIco a b
                  @[deprecated Set.notMem_Ico_of_ge (since := "2025-05-23")]
                  theorem Set.not_mem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b c) :
                  cIco a b

                  Alias of Set.notMem_Ico_of_ge.

                  theorem Set.notMem_Ioo_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c a) :
                  cIoo a b
                  @[deprecated Set.notMem_Ioo_of_le (since := "2025-05-23")]
                  theorem Set.not_mem_Ioo_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c a) :
                  cIoo a b

                  Alias of Set.notMem_Ioo_of_le.

                  theorem Set.notMem_Ioo_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b c) :
                  cIoo a b
                  @[deprecated Set.notMem_Ioo_of_ge (since := "2025-05-23")]
                  theorem Set.not_mem_Ioo_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b c) :
                  cIoo a b

                  Alias of Set.notMem_Ioo_of_ge.

                  @[simp]
                  theorem Set.Icc_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b = Ioc a b ¬a b
                  @[simp]
                  theorem Set.Icc_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b = Ico a b ¬a b
                  @[simp]
                  theorem Set.Icc_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Icc a b = Ioo a b ¬a b
                  @[simp]
                  theorem Set.Ioc_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b = Ico a b ¬a < b
                  @[simp]
                  theorem Set.Ioo_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b = Ioc a b ¬a < b
                  @[simp]
                  theorem Set.Ioo_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b = Ico a b ¬a < b
                  @[simp]
                  theorem Set.Ioc_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b = Icc a b ¬a b
                  @[simp]
                  theorem Set.Ico_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b = Icc a b ¬a b
                  @[simp]
                  theorem Set.Ioo_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioo a b = Icc a b ¬a b
                  @[simp]
                  theorem Set.Ico_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b = Ioc a b ¬a < b
                  @[simp]
                  theorem Set.Ioc_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ioc a b = Ioo a b ¬a < b
                  @[simp]
                  theorem Set.Ico_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
                  Ico a b = Ioo a b ¬a < b
                  @[simp]
                  theorem Set.Icc_self {α : Type u_1} [PartialOrder α] (a : α) :
                  Icc a a = {a}
                  instance Set.instIccUnique {α : Type u_1} [PartialOrder α] {a : α} :
                  Unique (Icc a a)
                  Equations
                    @[simp]
                    theorem Set.Icc_eq_singleton_iff {α : Type u_1} [PartialOrder α] {a b c : α} :
                    Icc a b = {c} a = c b = c
                    theorem Set.subsingleton_Icc_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (hba : b a) :
                    @[simp]
                    theorem Set.subsingleton_Icc_iff {α : Type u_2} [LinearOrder α] {a b : α} :
                    @[simp]
                    theorem Set.Icc_diff_left {α : Type u_1} [PartialOrder α] {a b : α} :
                    Icc a b \ {a} = Ioc a b
                    @[simp]
                    theorem Set.Icc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} :
                    Icc a b \ {b} = Ico a b
                    @[simp]
                    theorem Set.Ico_diff_left {α : Type u_1} [PartialOrder α] {a b : α} :
                    Ico a b \ {a} = Ioo a b
                    @[simp]
                    theorem Set.Ioc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} :
                    Ioc a b \ {b} = Ioo a b
                    @[simp]
                    theorem Set.Icc_diff_both {α : Type u_1} [PartialOrder α] {a b : α} :
                    Icc a b \ {a, b} = Ioo a b
                    @[simp]
                    theorem Set.Ici_diff_left {α : Type u_1} [PartialOrder α] {a : α} :
                    Ici a \ {a} = Ioi a
                    @[simp]
                    theorem Set.Iic_diff_right {α : Type u_1} [PartialOrder α] {a : α} :
                    Iic a \ {a} = Iio a
                    @[simp]
                    theorem Set.Ico_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
                    Ico a b \ Ioo a b = {a}
                    @[simp]
                    theorem Set.Ioc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
                    Ioc a b \ Ioo a b = {b}
                    @[simp]
                    theorem Set.Icc_diff_Ico_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    Icc a b \ Ico a b = {b}
                    @[simp]
                    theorem Set.Icc_diff_Ioc_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    Icc a b \ Ioc a b = {a}
                    @[simp]
                    theorem Set.Icc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    Icc a b \ Ioo a b = {a, b}
                    @[simp]
                    theorem Set.Ici_diff_Ioi_same {α : Type u_1} [PartialOrder α] {a : α} :
                    Ici a \ Ioi a = {a}
                    @[simp]
                    theorem Set.Iic_diff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} :
                    Iic a \ Iio a = {a}
                    theorem Set.Ioi_union_left {α : Type u_1} [PartialOrder α] {a : α} :
                    Ioi a {a} = Ici a
                    theorem Set.Iio_union_right {α : Type u_1} [PartialOrder α] {a : α} :
                    Iio a {a} = Iic a
                    theorem Set.Ioo_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) :
                    Ioo a b {a} = Ico a b
                    theorem Set.Ioo_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) :
                    Ioo a b {b} = Ioc a b
                    theorem Set.Ioo_union_both {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    Ioo a b {a, b} = Icc a b
                    theorem Set.Ioc_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a b) :
                    Ioc a b {a} = Icc a b
                    theorem Set.Ico_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a b) :
                    Ico a b {b} = Icc a b
                    @[simp]
                    theorem Set.Ico_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    insert b (Ico a b) = Icc a b
                    @[simp]
                    theorem Set.Ioc_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a b) :
                    insert a (Ioc a b) = Icc a b
                    @[simp]
                    theorem Set.Ioo_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
                    insert a (Ioo a b) = Ico a b
                    @[simp]
                    theorem Set.Ioo_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
                    insert b (Ioo a b) = Ioc a b
                    @[simp]
                    theorem Set.Iio_insert {α : Type u_1} [PartialOrder α] {a : α} :
                    insert a (Iio a) = Iic a
                    @[simp]
                    theorem Set.Ioi_insert {α : Type u_1} [PartialOrder α] {a : α} :
                    insert a (Ioi a) = Ici a
                    theorem Set.mem_Ici_Ioi_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Ioi a s) (hc : s Ici a) :
                    s {Ici a, Ioi a}
                    theorem Set.mem_Iic_Iio_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Iio a s) (hc : s Iic a) :
                    s {Iic a, Iio a}
                    theorem Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a b : α} {s : Set α} (ho : Ioo a b s) (hc : s Icc a b) :
                    s {Icc a b, Ico a b, Ioc a b, Ioo a b}
                    theorem Set.eq_left_or_mem_Ioo_of_mem_Ico {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x Ico a b) :
                    x = a x Ioo a b
                    theorem Set.eq_right_or_mem_Ioo_of_mem_Ioc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x Ioc a b) :
                    x = b x Ioo a b
                    theorem Set.eq_endpoints_or_mem_Ioo_of_mem_Icc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x Icc a b) :
                    x = a x = b x Ioo a b
                    theorem IsMax.Ici_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMax a) :
                    theorem IsMin.Iic_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMin a) :
                    theorem Set.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} :
                    Ici a = Ici b a = b
                    theorem Set.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} :
                    Iic a = Iic b a = b
                    @[simp]
                    theorem Set.Icc_inter_Icc_eq_singleton {α : Type u_1} [PartialOrder α] {a b c : α} (hab : a b) (hbc : b c) :
                    Icc a b Icc b c = {b}
                    theorem Set.Icc_eq_Icc_iff {α : Type u_1} [PartialOrder α] {a b c d : α} (h : a b) :
                    Icc a b = Icc c d a = c b = d
                    @[simp]
                    theorem Set.Ici_top {α : Type u_1} [PartialOrder α] [OrderTop α] :
                    theorem Set.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :
                    @[simp]
                    theorem Set.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :
                    @[simp]
                    theorem Set.Icc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
                    Icc a = Ici a
                    @[simp]
                    theorem Set.Ioc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
                    Ioc a = Ioi a
                    @[simp]
                    theorem Set.Iic_bot {α : Type u_1} [PartialOrder α] [OrderBot α] :
                    theorem Set.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                    @[simp]
                    theorem Set.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                    @[simp]
                    theorem Set.Icc_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
                    Icc a = Iic a
                    @[simp]
                    theorem Set.Ico_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
                    Ico a = Iio a
                    @[simp]
                    theorem Set.Iic_inter_Iic {α : Type u_1} [SemilatticeInf α] {a b : α} :
                    Iic a Iic b = Iic (ab)
                    @[simp]
                    theorem Set.Ioc_inter_Iic {α : Type u_1} [SemilatticeInf α] (a b c : α) :
                    Ioc a b Iic c = Ioc a (bc)
                    @[simp]
                    theorem Set.Ici_inter_Ici {α : Type u_1} [SemilatticeSup α] {a b : α} :
                    Ici a Ici b = Ici (ab)
                    @[simp]
                    theorem Set.Ico_inter_Ici {α : Type u_1} [SemilatticeSup α] (a b c : α) :
                    Ico a b Ici c = Ico (ac) b
                    theorem Set.Icc_inter_Icc {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} :
                    Icc a₁ b₁ Icc a₂ b₂ = Icc (a₁a₂) (b₁b₂)

                    Closed intervals in α × β #

                    @[simp]
                    theorem Set.Iic_prod_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
                    Iic a ×ˢ Iic b = Iic (a, b)
                    @[simp]
                    theorem Set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
                    Ici a ×ˢ Ici b = Ici (a, b)
                    theorem Set.Ici_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) :
                    theorem Set.Iic_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) :
                    @[simp]
                    theorem Set.Icc_prod_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) :
                    Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)
                    theorem Set.Icc_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a b : α × β) :
                    Icc a b = Icc a.fst b.fst ×ˢ Icc a.snd b.snd

                    Lemmas about intervals in dense orders #

                    instance instNoMinOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
                    instance instNoMinOrderElemIoc (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
                    instance instNoMinOrderElemIoi (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :
                    instance instNoMaxOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
                    instance instNoMaxOrderElemIco (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
                    instance instNoMaxOrderElemIio (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :

                    Intervals in Prop #

                    @[simp]