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.

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

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

• Set.decidableMemIoo = inst✝

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

Equations

• Set.decidableMemIco = inst✝

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

Equations

• Set.decidableMemIio = inst✝

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

Equations

• Set.decidableMemIcc = inst✝

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

Equations

• Set.decidableMemIic = inst✝

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

Equations

• Set.decidableMemIoc = inst✝

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

Equations

• Set.decidableMemIci = inst✝

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

Equations

• Set.decidableMemIoi = inst✝

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

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

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

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

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

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 : α} : Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Iic a

@[deprecated Set.Ici_toDual (since := "2025-03-20")]

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

Alias of Set.Ici_toDual.

@[simp]

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

@[deprecated Set.Iic_toDual (since := "2025-03-20")]

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

Alias of Set.Iic_toDual.

@[simp]

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

@[deprecated Set.Ioi_toDual (since := "2025-03-20")]

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

Alias of Set.Ioi_toDual.

@[simp]

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

@[deprecated Set.Iio_toDual (since := "2025-03-20")]

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

Alias of Set.Iio_toDual.

@[simp]

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

@[deprecated Set.Icc_toDual (since := "2025-03-20")]

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

Alias of Set.Icc_toDual.

@[simp]

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

@[deprecated Set.Ioc_toDual (since := "2025-03-20")]

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

Alias of Set.Ioc_toDual.

@[simp]

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

@[deprecated Set.Ico_toDual (since := "2025-03-20")]

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

Alias of Set.Ico_toDual.

@[simp]

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

@[deprecated Set.Ioo_toDual (since := "2025-03-20")]

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

Alias of Set.Ioo_toDual.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Set.Iio_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} : Iio (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioi 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_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 : α} : (Ici a).Nonempty

@[simp]

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

@[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 α] : (Ioi a).Nonempty

@[simp]

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

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 α] : NoMinOrder ↑(Iio a)

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

instance Set.instNoMaxOrderElemIoi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : NoMaxOrder ↑(Ioi 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 : ¬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 ≤ a → Set.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 < a → Set.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 ≤ b → Set.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 < b → Set.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) : 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.Ioi_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} : Ioi a = ∅ ↔ IsMax a

@[simp]

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

@[simp]

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

Alias of the reverse direction of Set.Ioi_eq_empty_iff.

@[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 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.not_mem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) : c ∉ Icc a b

theorem Set.not_mem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) : c ∉ Icc a b

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

theorem Set.not_mem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) : c ∉ Ioc a b

theorem Set.not_mem_Ioi_self {α : Type u_1} [Preorder α] {a : α} : a ∉ Ioi a

theorem Set.not_mem_Iio_self {α : Type u_1} [Preorder α] {b : α} : b ∉ Iio b

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

theorem Set.not_mem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b ≤ c) : c ∉ Ico a b

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

theorem Set.not_mem_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

• 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_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) : Set.Ici a = {a}

theorem IsMin.Iic_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMin a) : Set.Iic a = {a}

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

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

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}

@[simp]

theorem Set.Ici_top {α : Type u_1} [PartialOrder α] [OrderTop α] : Ici ⊤ = {⊤}

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

@[simp]

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

@[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 α] : Iic ⊥ = {⊥}

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

@[simp]

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

@[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.Ioc_inter_Iic {α : Type u_1} [SemilatticeInf α] (a b c : α) : Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

@[simp]

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

@[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.Ici_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Ici a = Ici a.fst ×ˢ Ici a.snd

theorem Set.Iic_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Iic a = Iic a.fst ×ˢ Iic a.snd

@[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 : α} : 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 : Ioi True = ∅