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:

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.

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

Decidable (x ∈ Iio b)

Equations

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

Decidable (x ∈ Ioi b)

Equations

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

Decidable (x ∈ Iic b)

Equations

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

Decidable (x ∈ Ici b)

Equations

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.decidableMemIcc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x ∧ x ≤ b)] :

Decidable (x ∈ Icc a b)

Equations

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

Decidable (x ∈ Ioc a b)

Equations

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 : α} :

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

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

a ∉ Ioo a b

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

a ∉ Ioc a b

@[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.left_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :

a ∈ Icc a b ↔ a ≤ b

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

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

Alias of Set.self_mem_Ici.

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

b ∉ Ioo a b

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

b ∉ Ico a b

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

theorem Set.right_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Ioc a b ↔ a < b

theorem Set.right_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :

b ∈ Icc a b ↔ a ≤ b

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

theorem Set.right_mem_Iic {α : Type u_1} [Preorder α] {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.Ioc_toDual {α : Type u_1} [Preorder α] {a b : α} :

Ioc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ico 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.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 y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ico x y

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

@[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_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)

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

Nonempty ↑(Ioo a b)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Set.Ico_self {α : Type u_1} [Preorder α] (a : α) :

theorem Set.Ioc_self {α : Type u_1} [Preorder α] (a : α) :

theorem Set.Ioo_self {α : Type u_1} [Preorder α] (a : α) :

@[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.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.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.Ico_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} :

Ico a b ⊆ Ici a

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

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

theorem Set.mem_Iic_of_Iio {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Iio 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) :

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.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 : α} (hb : b < c) :

c ∉ Icc a b

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 : α} (hb : b < c) :

c ∉ Ioc a b

@[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 : α} (hb : b ≤ c) :

c ∉ Ico a b

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 : α} (hb : b ≤ c) :

c ∉ Ioo a b

@[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) :

(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_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.Iic_diff_right {α : Type u_1} [PartialOrder α] {a : α} :

Iic a \ {a} = Iio a

@[simp]

theorem Set.Ici_diff_left {α : Type u_1} [PartialOrder α] {a : α} :

Ici a \ {a} = Ioi 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.Iic_diff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} :

Iic a \ Iio a = {a}

@[simp]

theorem Set.Ici_diff_Ioi_same {α : Type u_1} [PartialOrder α] {a : α} :

Ici a \ Ioi a = {a}

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 : 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_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 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 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 α] :

theorem Set.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :

@[simp]

theorem Set.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :

@[simp]

theorem Set.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :

@[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.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

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 α] (a b c : α) :

Ico a b ∩ Ici c = Ico (a ⊔ c) 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.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 instNoMinOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :

NoMinOrder ↑(Set.Ioo x y)

instance instNoMinOrderElemIoc (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :

NoMinOrder ↑(Set.Ioc x y)

instance instNoMinOrderElemIoi (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :

NoMinOrder ↑(Set.Ioi x)

instance instNoMaxOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :

NoMaxOrder ↑(Set.Ioo x y)

instance instNoMaxOrderElemIco (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :

NoMaxOrder ↑(Set.Ico x y)

instance instNoMaxOrderElemIio (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :

NoMaxOrder ↑(Set.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 :