Intervals

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

• i: infinite
• o: open
• c: closed

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).

A conscious decision was made not to list all possible inclusion relations. Monotonicity results and "self" results are included. Most use cases can suffice with a transitive combination of those, for example:

theorem Ico_subset_Ici (h : a₂ ≤ a₁) : Ico a₁ b₁ ⊆ Ici a₂ :=
  (Ico_subset_Ico_left h).trans Ico_subset_Ici_self

Logical equivalences, such as Icc_subset_Ici_iff, are however stated.

@[implicit_reducible]

instance Set.decidableMemIio {α : Type u_1} [Preorder α] {b x : α} [Decidable (x < b)] : Decidable (x ∈ Iio b)

Equations

• Set.decidableMemIio = inst✝

@[implicit_reducible]

instance Set.decidableMemIoi {α : Type u_1} [Preorder α] {b x : α} [Decidable (b < x)] : Decidable (x ∈ Ioi b)

Equations

• Set.decidableMemIoi = inst✝

@[implicit_reducible]

instance Set.decidableMemIic {α : Type u_1} [Preorder α] {b x : α} [Decidable (x ≤ b)] : Decidable (x ∈ Iic b)

Equations

• Set.decidableMemIic = inst✝

@[implicit_reducible]

instance Set.decidableMemIci {α : Type u_1} [Preorder α] {b x : α} [Decidable (b ≤ x)] : Decidable (x ∈ Ici b)

Equations

• Set.decidableMemIci = inst✝

@[implicit_reducible]

instance Set.decidableMemIoo {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x)] [Decidable (x < b)] : Decidable (x ∈ Ioo a b)

Equations

• Set.decidableMemIoo = instDecidableAnd

@[implicit_reducible]

instance Set.decidableMemIco {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x)] [Decidable (x < b)] : Decidable (x ∈ Ico a b)

Equations

• Set.decidableMemIco = instDecidableAnd

@[implicit_reducible]

instance Set.decidableMemIcc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x)] [Decidable (x ≤ b)] : Decidable (x ∈ Icc a b)

Equations

• Set.decidableMemIcc = instDecidableAnd

@[implicit_reducible]

instance Set.decidableMemIoc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x)] [Decidable (x ≤ b)] : Decidable (x ∈ Ioc a b)

Equations

• Set.decidableMemIoc = instDecidableAnd

theorem Set.self_notMem_Iio {α : Type u_1} [Preorder α] {a : α} : ¬a ∈ Iio a

theorem Set.self_notMem_Ioi {α : Type u_1} [Preorder α] {a : α} : ¬a ∈ Ioi a

theorem Set.self_mem_Iic {α : Type u_1} [Preorder α] {a : α} : a ∈ Iic a

theorem Set.self_mem_Ici {α : Type u_1} [Preorder α] {a : α} : a ∈ Ici a

theorem Set.left_notMem_Ioo {α : Type u_1} [Preorder α] {a b : α} : ¬a ∈ Ioo a b

theorem Set.right_notMem_Ioo {α : Type u_1} [Preorder α] {a b : α} : ¬a ∈ Ioo b a

theorem Set.left_notMem_Ioc {α : Type u_1} [Preorder α] {a b : α} : ¬a ∈ Ioc a b

theorem Set.right_notMem_Ico {α : Type u_1} [Preorder α] {a b : α} : ¬a ∈ Ico b a

@[deprecated Set.left_notMem_Ioo (since := "2025-12-26")]

theorem Set.left_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} : a ∈ Ioo a b ↔ False

@[deprecated Set.left_notMem_Ioc (since := "2025-12-26")]

theorem Set.left_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Ioc a b ↔ False

theorem Set.left_mem_Ico {α : Type u_1} [Preorder α] {a b : α} : a ∈ Ico a b ↔ a < b

theorem Set.right_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Ioc b a ↔ b < a

theorem Set.left_mem_Icc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Icc a b ↔ a ≤ b

theorem Set.right_mem_Icc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Icc b a ↔ b ≤ a

@[deprecated Set.self_mem_Ici (since := "2025-12-26")]

theorem Set.left_mem_Ici {α : Type u_1} [Preorder α] {a : α} : a ∈ Ici a

Alias of Set.self_mem_Ici.

@[deprecated Set.right_notMem_Ioo (since := "2025-12-26")]

theorem Set.right_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} : b ∈ Ioo a b ↔ False

@[deprecated Set.right_notMem_Ico (since := "2025-12-26")]

theorem Set.right_mem_Ico {α : Type u_1} [Preorder α] {a b : α} : b ∈ Ico a b ↔ False

@[deprecated Set.self_mem_Iic (since := "2025-12-26")]

theorem Set.right_mem_Iic {α : Type u_1} [Preorder α] {a : α} : a ∈ Iic a

Alias of Set.self_mem_Iic.

@[simp]

theorem Set.Iio_toDual {α : Type u_1} [Preorder α] {a : α} : Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Ioi a

@[simp]

theorem Set.Ioi_toDual {α : Type u_1} [Preorder α] {a : α} : Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Iio a

@[simp]

theorem Set.Iic_toDual {α : Type u_1} [Preorder α] {a : α} : Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Ici a

@[simp]

theorem Set.Ici_toDual {α : Type u_1} [Preorder α] {a : α} : Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Iic a

@[simp]

theorem Set.Icc_toDual {α : Type u_1} [Preorder α] {a b : α} : Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Icc b a

@[simp]

theorem Set.Ico_toDual {α : Type u_1} [Preorder α] {a b : α} : Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ioc b a

@[simp]

theorem Set.Ioc_toDual {α : Type u_1} [Preorder α] {a b : α} : Ioc (OrderDual.toDual b) (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Ico a b

@[simp]

theorem Set.Ioo_toDual {α : Type u_1} [Preorder α] {a b : α} : Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ioo b a

@[simp]

theorem Set.Iio_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Iio (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioi x

@[simp]

theorem Set.Ioi_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Ioi (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Iio x

@[simp]

theorem Set.Iic_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Iic (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ici x

@[simp]

theorem Set.Ici_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Ici (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Iic x

@[simp]

theorem Set.Icc_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Icc (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Icc x y

@[simp]

theorem Set.Ico_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Ico (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioc x y

@[simp]

theorem Set.Ioc_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Ioc (OrderDual.ofDual x) (OrderDual.ofDual y) = ⇑OrderDual.toDual ⁻¹' Ico y x

@[simp]

theorem Set.Ioo_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} : Ioo (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioo x y

@[simp]

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

@[simp]

theorem Set.nonempty_Ioi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : (Ioi a).Nonempty

@[simp]

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

@[simp]

theorem Set.nonempty_Ici {α : Type u_1} [Preorder α] {a : α} : (Ici a).Nonempty

@[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 b a).Nonempty ↔ b < a

@[simp]

theorem Set.nonempty_Ioo {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b

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.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_Iic_subtype {α : Type u_1} [Preorder α] {a : α} : Nonempty ↑(Iic a)

An interval Iic a is nonempty.

instance Set.nonempty_Ici_subtype {α : Type u_1} [Preorder α] {a : α} : Nonempty ↑(Ici a)

An interval Ici a is nonempty.

theorem Set.nonempty_Icc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : Nonempty ↑(Icc a b)

theorem Set.nonempty_Ioc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : Nonempty ↑(Ioc a b)

theorem Set.nonempty_Ico_subtype {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : Nonempty ↑(Ico b a)

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

@[simp]

theorem Set.Iio_one_eq_empty {α : Type u_1} [Preorder α] [One α] [IsBotOneClass α] : Iio 1 = ∅

@[simp]

theorem Set.Iio_zero_eq_empty {α : Type u_1} [Preorder α] [Zero α] [IsBotZeroClass α] : Iio 0 = ∅

instance Set.isEmpty_Iio_one {α : Type u_1} [Preorder α] [One α] [IsBotOneClass α] : IsEmpty ↑(Iio 1)

instance Set.isEmpty_Iio_zero {α : Type u_1} [Preorder α] [Zero α] [IsBotZeroClass α] : IsEmpty ↑(Iio 0)

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

instance Set.instNoMaxOrderElemIoi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : NoMaxOrder ↑(Ioi a)

instance Set.instNoMinOrderElemIic {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] : NoMinOrder ↑(Iic a)

instance Set.instNoMaxOrderElemIci {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : NoMaxOrder ↑(Ici a)

@[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 : ¬b < a) : Ioc b a = ∅

@[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 : a ≤ b) : Ioc b a = ∅

@[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 = ∅

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.Ioi_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : Ioi a ⊆ Ioi b

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.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.Ioi_ssubset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : Ioi a ⊂ Ioi b

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.

@[simp]

theorem Set.Iic_subset_Iic {α : Type u_1} [Preorder α] {a b : α} : Iic a ⊆ Iic b ↔ a ≤ b

@[simp]

theorem Set.Ici_subset_Ici {α : Type u_1} [Preorder α] {a b : α} : Ici a ⊆ Ici b ↔ b ≤ a

@[simp]

theorem Set.Iic_ssubset_Iic {α : Type u_1} [Preorder α] {a b : α} : Iic a ⊂ Iic b ↔ a < b

@[simp]

theorem Set.Ici_ssubset_Ici {α : Type u_1} [Preorder α] {a b : α} : Ici a ⊂ Ici b ↔ b < a

@[simp]

theorem Set.Iic_subset_Iio {α : Type u_1} [Preorder α] {a b : α} : Iic a ⊆ Iio b ↔ a < b

@[simp]

theorem Set.Ici_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} : Ici a ⊆ Ioi b ↔ b < a

theorem Set.Iio_subset_Iic_self {α : Type u_1} [Preorder α] {a : α} : Iio a ⊆ Iic a

theorem Set.Ioi_subset_Ici_self {α : Type u_1} [Preorder α] {a : α} : Ioi a ⊆ Ici a

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.Ioi_subset_Ici {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : Ioi a ⊆ Ici b

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_ssubset_Iic_self {α : Type u_1} [Preorder α] {a : α} : Iio a ⊂ Iic a

theorem Set.Ioi_ssubset_Ici_self {α : Type u_1} [Preorder α] {a : α} : Ioi a ⊂ Ici a

theorem Set.Ioo_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ ≤ a₁) (hb : 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₁ a₂ b : α} (h : a₂ ≤ a₁) : Ioo b a₂ ⊆ Ioo b a₁

theorem Set.Ico_subset_Ico {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂

theorem Set.Ioc_subset_Ioc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hb : b₂ ≤ b₁) (ha : a₁ ≤ a₂) : Ioc b₁ a₁ ⊆ Ioc b₂ a₂

theorem Set.Ico_subset_Ico_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b

theorem Set.Ioc_subset_Ioc_right {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₂ ≤ a₁) : Ioc b a₂ ⊆ Ioc b a₁

theorem Set.Ioc_subset_Ioc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Ioc a₂ b ⊆ Ioc a₁ b

theorem Set.Ico_subset_Ico_right {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₂ ≤ a₁) : Ico b a₂ ⊆ Ico b a₁

theorem Set.Icc_subset_Icc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ ≤ a₁) (hb : 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₁ a₂ b : α} (h : a₂ ≤ a₁) : Icc b a₂ ⊆ Icc b a₁

theorem Set.Icc_ssubset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₂ : 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₂ : α} (h₂ : b₂ ≤ a₂) (hb : b₂ ≤ b₁) (ha : a₁ < a₂) : Icc b₁ a₁ ⊂ Icc b₂ a₂

theorem Set.Ico_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ioo a₂ b₂

theorem Set.Ioc_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hb : b₂ ≤ b₁) (ha : a₁ < a₂) : Ioc b₁ a₁ ⊆ Ioo b₂ a₂

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₁ a₂ b : α} (h : a₂ < a₁) : Ioc b a₂ ⊆ Ioo b a₁

theorem Set.Icc_subset_Ioc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Ioc a₂ b₂

theorem Set.Icc_subset_Ico {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hb : b₂ ≤ b₁) (ha : a₁ < a₂) : Icc b₁ a₁ ⊆ Ico b₂ a₂

theorem Set.Icc_subset_Ioc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ < a₂) : Icc a₂ b ⊆ Ioc a₁ b

theorem Set.Icc_subset_Ico_right {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₂ < a₁) : Icc b a₂ ⊆ Ico b a₁

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.Ico_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} : Ico a b ⊆ Iio b

theorem Set.Ioc_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} : Ioc b a ⊆ Ioi b

theorem Set.Ioo_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} : Ioo a b ⊆ Iio b

theorem Set.Ioo_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} : Ioo b a ⊆ Ioi b

theorem Set.Ioc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} : Ioc a b ⊆ Iic b

theorem Set.Ico_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} : Ico b a ⊆ Ici b

theorem Set.Icc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} : Icc a b ⊆ Iic b

theorem Set.Icc_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} : Icc b a ⊆ Ici 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 b a ⊆ Ioc b a

theorem Set.Ioc_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Ioc a b ⊆ Icc a b

theorem Set.Ico_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Ico b a ⊆ Icc b a

theorem Set.Ioo_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Ioo a b ⊆ Icc a b

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_Ioi_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁

theorem Set.Icc_subset_Iio_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : b₁ ≤ a₁) : Icc b₁ a₁ ⊆ Iio a₂ ↔ a₁ < a₂

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_subset_Iic_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : b₁ ≤ a₁) : Icc b₁ a₁ ⊆ Iic a₂ ↔ a₁ ≤ a₂

theorem Set.Ici_inter_Iic {α : Type u_1} [Preorder α] {a b : α} : Ici a ∩ Iic b = Icc a b

theorem Set.Iic_inter_Ici {α : Type u_1} [Preorder α] {a b : α} : Iic a ∩ Ici b = Icc b a

theorem Set.Ici_inter_Iio {α : Type u_1} [Preorder α] {a b : α} : Ici a ∩ Iio b = Ico a b

theorem Set.Iic_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} : Iic a ∩ Ioi b = Ioc b a

theorem Set.Ioi_inter_Iic {α : Type u_1} [Preorder α] {a b : α} : Ioi a ∩ Iic b = Ioc a b

theorem Set.Iio_inter_Ici {α : Type u_1} [Preorder α] {a b : α} : Iio a ∩ Ici b = Ico b a

theorem Set.Ioi_inter_Iio {α : Type u_1} [Preorder α] {a b : α} : Ioi a ∩ Iio b = Ioo a b

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 b a) : x ∈ Ioc b a

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_Icc_of_Ico {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ico b a) : x ∈ Icc b a

theorem Set.mem_Iic_of_Iio {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Iio a) : x ∈ Iic a

theorem Set.mem_Ici_of_Ioi {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Ioi a) : x ∈ Ici 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 b a = ∅ ↔ ¬b < a

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) : Set.Iic a = Set.univ

theorem IsBot.Ici_eq {α : Type u_1} [Preorder α] {a : α} (h : IsBot a) : Set.Ici a = Set.univ

@[simp]

theorem Set.Iio_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} : Iio a = ∅ ↔ IsMin a

@[simp]

theorem Set.Ioi_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} : Ioi a = ∅ ↔ IsMax a

@[simp]

theorem IsMin.Iio_eq {α : Type u_1} [Preorder α] {a : α} : IsMin a → Set.Iio a = ∅

Alias of the reverse direction of Set.Iio_eq_empty_iff.

@[simp]

theorem IsMax.Ioi_eq {α : Type u_1} [Preorder α] {a : α} : IsMax a → Set.Ioi a = ∅

@[simp]

theorem Set.Iio_nonempty {α : Type u_1} [Preorder α] {a : α} : (Iio a).Nonempty ↔ ¬IsMin a

@[simp]

theorem Set.Ioi_nonempty {α : Type u_1} [Preorder α] {a : α} : (Ioi a).Nonempty ↔ ¬IsMax 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.Ici_inter_Ico_of_le {α : Type u_1} [Preorder α] {a b c : α} (h : c ≤ a) : Ici a ∩ Ico c b = Ico a b

theorem Set.notMem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) : ¬c ∈ Icc a b

theorem Set.notMem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (ha : a < c) : ¬c ∈ Icc b a

theorem Set.notMem_Ico_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) : ¬c ∈ Ico a b

theorem Set.notMem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (ha : a < c) : ¬c ∈ Ioc b a

@[deprecated Set.self_notMem_Ioi (since := "2026-02-10")]

theorem Set.notMem_Ioi_self {α : Type u_1} [Preorder α] {a : α} : ¬a ∈ Ioi a

Alias of Set.self_notMem_Ioi.

@[deprecated Set.self_notMem_Iio (since := "2026-02-10")]

theorem Set.notMem_Iio_self {α : Type u_1} [Preorder α] {a : α} : ¬a ∈ Iio a

Alias of Set.self_notMem_Iio.

theorem Set.notMem_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) : ¬c ∈ Ioc a b

theorem Set.notMem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (ha : a ≤ c) : ¬c ∈ Ico b a

theorem Set.notMem_Ioo_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) : ¬c ∈ Ioo a b

theorem Set.notMem_Ioo_of_ge {α : Type u_1} [Preorder α] {a b c : α} (ha : a ≤ c) : ¬c ∈ Ioo b a

@[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 b a = Ico b a ↔ ¬b ≤ a

@[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 b a = Icc b a ↔ ¬b ≤ a

@[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.Ioo_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} : Ioo a b = Icc 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.Ico_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} : Ico b a = Ioc b a ↔ ¬b < a

@[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 b a = Ico b a ↔ ¬b < a

@[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 b a = Ioo b a ↔ ¬b < a

@[simp]

theorem Set.Icc_self {α : Type u_1} [PartialOrder α] (a : α) : Icc a a = {a}

@[implicit_reducible]

instance Set.instIccUnique {α : Type u_1} [PartialOrder α] {a : α} : Unique ↑(Icc a a)

Equations

• Set.instIccUnique = { default := ⟨a, ⋯⟩, uniq := ⋯ }

@[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) : (Icc a b).Subsingleton

@[simp]

theorem Set.subsingleton_Icc_iff {α : Type u_2} [LinearOrder α] {a b : α} : (Icc a b).Subsingleton ↔ b ≤ a

@[simp]

theorem Set.Icc_sdiff_left {α : Type u_1} [PartialOrder α] {a b : α} : Icc a b \ {a} = Ioc a b

@[simp]

theorem Set.Icc_sdiff_right {α : Type u_1} [PartialOrder α] {a b : α} : Icc b a \ {a} = Ico b a

@[deprecated Set.Icc_sdiff_left (since := "2026-06-03")]

theorem Set.Icc_diff_left {α : Type u_1} [PartialOrder α] {a b : α} : Icc a b \ {a} = Ioc a b

Alias of Set.Icc_sdiff_left.

@[simp]

theorem Set.Ico_sdiff_left {α : Type u_1} [PartialOrder α] {a b : α} : Ico a b \ {a} = Ioo a b

@[simp]

theorem Set.Ioc_sdiff_right {α : Type u_1} [PartialOrder α] {a b : α} : Ioc b a \ {a} = Ioo b a

@[deprecated Set.Ico_sdiff_left (since := "2026-06-03")]

theorem Set.Ico_diff_left {α : Type u_1} [PartialOrder α] {a b : α} : Ico a b \ {a} = Ioo a b

Alias of Set.Ico_sdiff_left.

@[simp]

theorem Set.Icc_sdiff_both {α : Type u_1} [PartialOrder α] {a b : α} : Icc a b \ {a, b} = Ioo a b

@[deprecated Set.Icc_sdiff_both (since := "2026-06-03")]

theorem Set.Icc_diff_both {α : Type u_1} [PartialOrder α] {a b : α} : Icc a b \ {a, b} = Ioo a b

Alias of Set.Icc_sdiff_both.

@[simp]

theorem Set.Iic_sdiff_right {α : Type u_1} [PartialOrder α] {a : α} : Iic a \ {a} = Iio a

@[simp]

theorem Set.Ici_sdiff_left {α : Type u_1} [PartialOrder α] {a : α} : Ici a \ {a} = Ioi a

@[deprecated Set.Iic_sdiff_right (since := "2026-06-03")]

theorem Set.Iic_diff_right {α : Type u_1} [PartialOrder α] {a : α} : Iic a \ {a} = Iio a

Alias of Set.Iic_sdiff_right.

@[simp]

theorem Set.Ico_sdiff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : Ico a b \ Ioo a b = {a}

@[simp]

theorem Set.Ioc_sdiff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : b < a) : Ioc b a \ Ioo b a = {a}

@[deprecated Set.Ico_sdiff_Ioo_same (since := "2026-06-03")]

theorem Set.Ico_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : Ico a b \ Ioo a b = {a}

Alias of Set.Ico_sdiff_Ioo_same.

@[simp]

theorem Set.Icc_sdiff_Ico_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Icc a b \ Ico a b = {b}

@[simp]

theorem Set.Icc_sdiff_Ioc_same {α : Type u_1} [PartialOrder α] {a b : α} (h : b ≤ a) : Icc b a \ Ioc b a = {b}

@[deprecated Set.Icc_sdiff_Ico_same (since := "2026-06-03")]

theorem Set.Icc_diff_Ico_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Icc a b \ Ico a b = {b}

Alias of Set.Icc_sdiff_Ico_same.

@[simp]

theorem Set.Icc_sdiff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Icc a b \ Ioo a b = {a, b}

@[deprecated Set.Icc_sdiff_Ioo_same (since := "2026-06-03")]

theorem Set.Icc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Icc a b \ Ioo a b = {a, b}

Alias of Set.Icc_sdiff_Ioo_same.

@[simp]

theorem Set.Iic_sdiff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} : Iic a \ Iio a = {a}

@[simp]

theorem Set.Ici_sdiff_Ioi_same {α : Type u_1} [PartialOrder α] {a : α} : Ici a \ Ioi a = {a}

@[deprecated Set.Iic_sdiff_Iio_same (since := "2026-06-03")]

theorem Set.Iic_diff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} : Iic a \ Iio a = {a}

Alias of Set.Iic_sdiff_Iio_same.

theorem Set.Iio_union_right {α : Type u_1} [PartialOrder α] {a : α} : Iio a ∪ {a} = Iic a

theorem Set.Ioi_union_left {α : Type u_1} [PartialOrder α] {a : α} : Ioi a ∪ {a} = Ici 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 : b < a) : Ioo b a ∪ {a} = Ioc b a

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 : b ≤ a) : Ico b a ∪ {a} = Icc b a

@[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 : b ≤ a) : insert b (Ioc b a) = Icc b a

@[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 : b < a) : insert a (Ioo b a) = Ioc b a

@[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_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_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_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 b a) : x = a ∨ x ∈ Ioo b a

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 IsMin.Iic_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMin a) : Set.Iic a = {a}

theorem IsMax.Ici_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMax a) : Set.Ici a = {a}

theorem Set.Iic_injective {α : Type u_1} [PartialOrder α] : Function.Injective Iic

theorem Set.Ici_injective {α : Type u_1} [PartialOrder α] : Function.Injective Ici

theorem Set.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} : Iic a = Iic b ↔ a = b

theorem Set.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} : Ici a = Ici 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 α] : Ici ⊤ = {⊤}

@[simp]

theorem Set.Iic_bot {α : Type u_1} [PartialOrder α] [OrderBot α] : Iic ⊥ = {⊥}

theorem Set.Iio_top {α : Type u_1} [PartialOrder α] [OrderTop α] : Iio ⊤ = {⊤}ᶜ

theorem Set.Ioi_bot {α : Type u_1} [PartialOrder α] [OrderBot α] : Ioi ⊥ = {⊥}ᶜ

theorem Set.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] : Ioi ⊤ = ∅

theorem Set.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] : Iio ⊥ = ∅

@[simp]

theorem Set.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] : Iic ⊤ = univ

@[simp]

theorem Set.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] : Ici ⊥ = univ

@[simp]

theorem Set.Icc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} : Icc a ⊤ = Ici a

@[simp]

theorem Set.Icc_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} : Icc ⊥ a = Iic a

@[simp]

theorem Set.Ioc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} : Ioc a ⊤ = Ioi a

@[simp]

theorem Set.Ico_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} : Ico ⊥ a = Iio a

theorem Set.Icc_bot_top {α : Type u_1} [Preorder α] [BoundedOrder α] : Icc ⊥ ⊤ = univ

@[simp]

theorem Set.Iic_inter_Iic {α : Type u_1} [SemilatticeInf α] {a b : α} : Iic a ∩ Iic b = Iic (a ⊓ b)

@[simp]

theorem Set.Ici_inter_Ici {α : Type u_1} [SemilatticeSup α] {a b : α} : Ici a ∩ Ici b = Ici (a ⊔ b)

@[simp]

theorem Set.Ioc_inter_Iic {α : Type u_1} [SemilatticeInf α] (a b c : α) : Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

@[simp]

theorem Set.Ico_inter_Ici {α : Type u_1} [SemilatticeSup α] (b a c : α) : Ico b a ∩ Ici c = Ico (b ⊔ c) a

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.Iic_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Iic a = Iic a.1 ×ˢ Iic a.2

theorem Set.Ici_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Ici a = Ici a.1 ×ˢ Ici a.2

@[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.1 b.1 ×ˢ Icc a.2 b.2

Lemmas about intervals in dense orders

instance Set.instNoMinOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMinOrder ↑(Ioo x y)

instance Set.instNoMaxOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMaxOrder ↑(Ioo y x)

instance Set.instNoMinOrderElemIoc (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMinOrder ↑(Ioc x y)

instance Set.instNoMaxOrderElemIco (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMaxOrder ↑(Ico y x)

instance Set.instNoMinOrderElemIoi (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} : NoMinOrder ↑(Ioi x)

instance Set.instNoMaxOrderElemIio (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} : NoMaxOrder ↑(Iio x)

Intervals in Prop

@[simp]

theorem Set.Iic_False : Iic False = {False}

@[simp]

theorem Set.Iic_True : Iic True = univ

@[simp]

theorem Set.Ici_False : Ici False = univ

@[simp]

theorem Set.Ici_True : Ici True = {True}

theorem Set.Iio_False : Iio False = ∅

@[simp]

theorem Set.Iio_True : Iio True = {False}

@[simp]

theorem Set.Ioi_False : Ioi False = {True}

theorem Set.Ioi_True : Ioi True = ∅