Documentation

Mathlib.Order.Interval.Set.LinearOrder

Interval properties in linear orders #

Since every pair of elements are comparable in a linear order, intervals over them are better behaved. This file collects their properties under this assumption.

source
theorem Set.notMem_Ici {α : Type u_1} [LinearOrder α] {a c : α} :
¬c ∈ Ici a ↔ c < a
source
theorem Set.notMem_Iic {α : Type u_1} [LinearOrder α] {a c : α} :
¬c ∈ Iic a ↔ a < c
source
theorem Set.notMem_Ioi {α : Type u_1} [LinearOrder α] {a c : α} :
¬c ∈ Ioi a ↔ c ≤ a
source
theorem Set.notMem_Iio {α : Type u_1} [LinearOrder α] {a c : α} :
¬c ∈ Iio a ↔ a ≤ c
source
@[simp]
theorem Set.compl_Iic {α : Type u_1} [LinearOrder α] {a : α} :
(Iic a)ᶜ = Ioi a
source
@[simp]
theorem Set.compl_Ici {α : Type u_1} [LinearOrder α] {a : α} :
(Ici a)ᶜ = Iio a
source
@[simp]
theorem Set.compl_Iio {α : Type u_1} [LinearOrder α] {a : α} :
(Iio a)ᶜ = Ici a
source
@[simp]
theorem Set.compl_Ioi {α : Type u_1} [LinearOrder α] {a : α} :
(Ioi a)ᶜ = Iic a
source
@[simp]
theorem Set.Ici_sdiff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ici b = Ico a b
source
@[simp]
theorem Set.Iic_sdiff_Iic {α : Type u_1} [LinearOrder α] {a b : α} :
Iic a \ Iic b = Ioc b a
source
@[deprecated Set.Ici_sdiff_Ici (since := "2026-06-03")]
theorem Set.Ici_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ici b = Ico a b

Alias of Set.Ici_sdiff_Ici.

source
@[simp]
theorem Set.Ici_sdiff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ioi b = Icc a b
source
@[simp]
theorem Set.Iic_sdiff_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iic a \ Iio b = Icc b a
source
@[deprecated Set.Ici_sdiff_Ioi (since := "2026-06-03")]
theorem Set.Ici_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ioi b = Icc a b

Alias of Set.Ici_sdiff_Ioi.

source
@[simp]
theorem Set.Ioi_sdiff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ioi b = Ioc a b
source
@[simp]
theorem Set.Iio_sdiff_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a \ Iio b = Ico b a
source
@[deprecated Set.Ioi_sdiff_Ioi (since := "2026-06-03")]
theorem Set.Ioi_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ioi b = Ioc a b

Alias of Set.Ioi_sdiff_Ioi.

source
@[simp]
theorem Set.Ioi_sdiff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ici b = Ioo a b
source
@[simp]
theorem Set.Iio_sdiff_Iic {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a \ Iic b = Ioo b a
source
@[deprecated Set.Ioi_sdiff_Ici (since := "2026-06-03")]
theorem Set.Ioi_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ici b = Ioo a b

Alias of Set.Ioi_sdiff_Ici.

source
theorem Set.Ioi_injective {α : Type u_1} [LinearOrder α] :
Function.Injective Ioi
source
theorem Set.Iio_injective {α : Type u_1} [LinearOrder α] :
Function.Injective Iio
source
theorem Set.Ioi_inj {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a = Ioi b ↔ a = b
source
theorem Set.Iio_inj {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a = Iio b ↔ a = b
source
theorem Set.Ico_subset_Ico_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) :
Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
theorem Set.Ioc_subset_Ioc_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) :
Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
source
theorem Set.Ico_eq_Ico_iff {α : Type u_1} [LinearOrder α] {a b c d : α} (h : a < b ∨ c < d) :
Ico a b = Ico c d ↔ a = c ∧ b = d
source
theorem Set.Ioc_eq_Ioc_iff {α : Type u_1} [LinearOrder α] {a b c d : α} (hab : a < b ∨ c < d) :
Ioc a b = Ioc c d ↔ a = c ∧ b = d
source
theorem Set.Ioo_subset_Ioo_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} [DenselyOrdered α] (h₁ : a₁ < b₁) :
Ioo a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
theorem Set.Ici_eq_singleton_iff_isTop {α : Type u_1} [LinearOrder α] {x : α} :
Ici x = {x} ↔ IsTop x
source
theorem Set.Iic_eq_singleton_iff_isBot {α : Type u_1} [LinearOrder α] {x : α} :
Iic x = {x} ↔ IsBot x
source
@[simp]
theorem Set.Ioi_subset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi b ⊆ Ioi a ↔ a ≤ b
source
@[simp]
theorem Set.Iio_subset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b ⊆ Iio a ↔ b ≤ a
source
@[simp]
theorem Set.Ioi_ssubset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi b ⊂ Ioi a ↔ a < b
source
@[simp]
theorem Set.Iio_ssubset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b ⊂ Iio a ↔ b < a
source
@[simp]
theorem Set.Ioi_subset_Ici_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] :
Ioi b ⊆ Ici a ↔ a ≤ b
source
@[simp]
theorem Set.Iio_subset_Iic_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] :
Iio b ⊆ Iic a ↔ b ≤ a

Two infinite intervals #

source
theorem Set.Iic_union_Ioi_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iic b ∪ Ioi a = univ
source
theorem Set.Ici_union_Iio_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
Ici b ∪ Iio a = univ
source
theorem Set.Iio_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iio b ∪ Ici a = univ
source
theorem Set.Ioi_union_Iic_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
Ioi b ∪ Iic a = univ
source
theorem Set.Iic_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iic b ∪ Ici a = univ
source
theorem Set.Ici_union_Iic_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
Ici b ∪ Iic a = univ
source
theorem Set.Iio_union_Ioi_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Iio b ∪ Ioi a = univ
source
theorem Set.Ioi_union_Iio_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) :
Ioi b ∪ Iio a = univ
source
@[simp]
theorem Set.Iic_union_Ici {α : Type u_1} [LinearOrder α] {a : α} :
Iic a ∪ Ici a = univ
source
@[simp]
theorem Set.Ici_union_Iic {α : Type u_1} [LinearOrder α] {a : α} :
Ici a ∪ Iic a = univ
source
@[simp]
theorem Set.Iio_union_Ici {α : Type u_1} [LinearOrder α] {a : α} :
Iio a ∪ Ici a = univ
source
@[simp]
theorem Set.Ioi_union_Iic {α : Type u_1} [LinearOrder α] {a : α} :
Ioi a ∪ Iic a = univ
source
@[simp]
theorem Set.Iic_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} :
Iic a ∪ Ioi a = univ
source
@[simp]
theorem Set.Ici_union_Iio {α : Type u_1} [LinearOrder α] {a : α} :
Ici a ∪ Iio a = univ
source
@[simp]
theorem Set.Iio_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} :
Iio a ∪ Ioi a = {a}ᶜ
source
@[simp]
theorem Set.Ioi_union_Iio {α : Type u_1} [LinearOrder α] {a : α} :
Ioi a ∪ Iio a = {a}ᶜ

A finite and an infinite interval #

source
theorem Set.Ioo_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c < max a b) :
Ioo a b ∪ Ioi c = Ioi (min a c)
source
theorem Set.Ioi_subset_Ioo_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a ⊆ Ioo a b ∪ Ici b
source
@[simp]
theorem Set.Ioo_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Ioo a b ∪ Ici b = Ioi a
source
theorem Set.Ici_subset_Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a ⊆ Ico a b ∪ Ici b
source
@[simp]
theorem Set.Ico_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Ico a b ∪ Ici b = Ici a
source
theorem Set.Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ max a b) :
Ico a b ∪ Ici c = Ici (min a c)
source
theorem Set.Ioi_subset_Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a ⊆ Ioc a b ∪ Ioi b
source
@[simp]
theorem Set.Ioc_union_Ioi_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Ioc a b ∪ Ioi b = Ioi a
source
theorem Set.Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ max a b) :
Ioc a b ∪ Ioi c = Ioi (min a c)
source
theorem Set.Ici_subset_Icc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a ⊆ Icc a b ∪ Ioi b
source
@[simp]
theorem Set.Icc_union_Ioi_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Icc a b ∪ Ioi b = Ici a
source
theorem Set.Ioi_subset_Ioc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a ⊆ Ioc a b ∪ Ici b
source
@[simp]
theorem Set.Ioc_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Ioc a b ∪ Ici b = Ioi a
source
theorem Set.Ici_subset_Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a ⊆ Icc a b ∪ Ici b
source
@[simp]
theorem Set.Icc_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Icc a b ∪ Ici b = Ici a
source
theorem Set.Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ max a b) :
Icc a b ∪ Ici c = Ici (min a c)
source
theorem Set.Ioo_union_Ioi_eq_Ioi_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b : α} (a_le_b : a ≤ b) :
Ioo a b ∪ Ioi b = Ioi a \ {b}
source
theorem Set.Ico_union_Ioi_eq_Ici_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b : α} (a_le_b : a ≤ b) :
Ico a b ∪ Ioi b = Ici a \ {b}

An infinite and a finite interval #

source
theorem Set.Iic_subset_Iio_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b ⊆ Iio a ∪ Icc a b
source
@[simp]
theorem Set.Iio_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iio a ∪ Icc a b = Iic b
source
theorem Set.Iio_subset_Iio_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b ⊆ Iio a ∪ Ico a b
source
@[simp]
theorem Set.Iio_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iio a ∪ Ico a b = Iio b
source
theorem Set.Iio_union_Ico {α : Type u_1} [LinearOrder α] {b c d : α} (h : min c d ≤ b) :
Iio b ∪ Ico c d = Iio (max b d)
source
theorem Set.Iic_subset_Iic_union_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b ⊆ Iic a ∪ Ioc a b
source
@[simp]
theorem Set.Iic_union_Ioc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iic a ∪ Ioc a b = Iic b
source
theorem Set.Iic_union_Ioc {α : Type u_1} [LinearOrder α] {b c d : α} (h : min c d < b) :
Iic b ∪ Ioc c d = Iic (max b d)
source
theorem Set.Iio_subset_Iic_union_Ioo {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b ⊆ Iic a ∪ Ioo a b
source
@[simp]
theorem Set.Iic_union_Ioo_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Iic a ∪ Ioo a b = Iio b
source
theorem Set.Iio_union_Ioo {α : Type u_1} [LinearOrder α] {b c d : α} (h : min c d < b) :
Iio b ∪ Ioo c d = Iio (max b d)
source
theorem Set.Iic_subset_Iic_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b ⊆ Iic a ∪ Icc a b
source
@[simp]
theorem Set.Iic_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iic a ∪ Icc a b = Iic b
source
theorem Set.Iic_union_Icc {α : Type u_1} [LinearOrder α] {b c d : α} (h : min c d ≤ b) :
Iic b ∪ Icc c d = Iic (max b d)
source
theorem Set.Iio_subset_Iic_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b ⊆ Iic a ∪ Ico a b
source
@[simp]
theorem Set.Iic_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Iic a ∪ Ico a b = Iio b
source
theorem Set.Iio_union_Ioo_eq_Iio_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b : α} (a_le_b : a ≤ b) :
Iio a ∪ Ioo a b = Iio b \ {a}
source
theorem Set.Iio_union_Ioc_eq_Iic_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b : α} (a_le_b : a ≤ b) :
Iio a ∪ Ioc a b = Iic b \ {a}

Two finite intervals, I?o and Ic? #

source
theorem Set.Ioo_subset_Ioo_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a c ⊆ Ioo a b ∪ Ico b c
source
@[simp]
theorem Set.Ioo_union_Ico_eq_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) :
Ioo a b ∪ Ico b c = Ioo a c
source
theorem Set.Ico_subset_Ico_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a c ⊆ Ico a b ∪ Ico b c
source
@[simp]
theorem Set.Ico_union_Ico_eq_Ico {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Ico a b ∪ Ico b c = Ico a c
source
theorem Set.Ico_union_Ico {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d)
source
theorem Set.Ico_union_Ico' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d)

This is a special case of Ico_union_Ico

source
theorem Set.Icc_subset_Ico_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} :
Icc a c ⊆ Ico a b ∪ Icc b c
source
@[simp]
theorem Set.Ico_union_Icc_eq_Icc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Ico a b ∪ Icc b c = Icc a c
source
theorem Set.Ioc_subset_Ioo_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a c ⊆ Ioo a b ∪ Icc b c
source
@[simp]
theorem Set.Ioo_union_Icc_eq_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) :
Ioo a b ∪ Icc b c = Ioc a c

Two finite intervals, I?c and Io? #

source
theorem Set.Ioo_subset_Ioc_union_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a c ⊆ Ioc a b ∪ Ioo b c
source
@[simp]
theorem Set.Ioc_union_Ioo_eq_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) :
Ioc a b ∪ Ioo b c = Ioo a c
source
theorem Set.Ico_subset_Icc_union_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a c ⊆ Icc a b ∪ Ioo b c
source
@[simp]
theorem Set.Icc_union_Ioo_eq_Ico {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) :
Icc a b ∪ Ioo b c = Ico a c
source
theorem Set.Icc_subset_Icc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} :
Icc a c ⊆ Icc a b ∪ Ioc b c
source
@[simp]
theorem Set.Icc_union_Ioc_eq_Icc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Icc a b ∪ Ioc b c = Icc a c
source
theorem Set.Ioc_subset_Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a c ⊆ Ioc a b ∪ Ioc b c
source
@[simp]
theorem Set.Ioc_union_Ioc_eq_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Ioc a b ∪ Ioc b c = Ioc a c
source
theorem Set.Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)
source
theorem Set.Ioc_union_Ioc' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

This is a special case of Ioc_union_Ioc

Two finite intervals with a common point #

source
theorem Set.Ioo_subset_Ioc_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a c ⊆ Ioc a b ∪ Ico b c
source
@[simp]
theorem Set.Ioc_union_Ico_eq_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) :
Ioc a b ∪ Ico b c = Ioo a c
source
@[simp]
theorem Set.Ico_union_Ioc_eq_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : b < a) (h₂ : c < b) :
Ico b a ∪ Ioc c b = Ioo c a
source
theorem Set.Ico_subset_Icc_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a c ⊆ Icc a b ∪ Ico b c
source
@[simp]
theorem Set.Icc_union_Ico_eq_Ico {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) :
Icc a b ∪ Ico b c = Ico a c
source
theorem Set.Icc_subset_Icc_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} :
Icc a c ⊆ Icc a b ∪ Icc b c
source
@[simp]
theorem Set.Icc_union_Icc_eq_Icc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Icc a b ∪ Icc b c = Icc a c
source
theorem Set.Icc_union_Icc' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
Icc a b ∪ Icc c d = Icc (min a c) (max b d)
source
theorem Set.Icc_union_Icc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
Icc a b ∪ Icc c d = Icc (min a c) (max b d)

We cannot replace < by ≤ in the hypotheses. Otherwise for b < a = d < c the l.h.s. is ∅ and the r.h.s. is {a}.

source
theorem Set.Ioc_subset_Ioc_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a c ⊆ Ioc a b ∪ Icc b c
source
@[simp]
theorem Set.Ioc_union_Icc_eq_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) :
Ioc a b ∪ Icc b c = Ioc a c
source
theorem Set.Ioo_union_Ioo' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c < b) (h₂ : a < d) :
Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
source
theorem Set.Ioo_union_Ioo {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)
source
theorem Set.Ioo_subset_Ioo_union_Ioo {α : Type u_1} [LinearOrder α] {a a₁ b b₁ c d : α} (h₁ : a ≤ a₁) (h₂ : c < b) (h₃ : b₁ ≤ d) :
Ioo a₁ b₁ ⊆ Ioo a b ∪ Ioo c d
source
theorem Set.Ioo_union_Ioo_eq_Ioo_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b c : α} (a_le_b : a ≤ b) (b_le_c : b ≤ c) :
Ioo a b ∪ Ioo b c = Ioo a c \ {b}
source
theorem Set.Ico_union_Ioo_eq_Ico_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b c : α} (a_le_b : a ≤ b) (b_le_c : b ≤ c) :
Ico a b ∪ Ioo b c = Ico a c \ {b}
source
theorem Set.Ico_union_Ioc_eq_Icc_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b c : α} (a_le_b : a ≤ b) (b_le_c : b ≤ c) :
Ico a b ∪ Ioc b c = Icc a c \ {b}
source
theorem Set.Ioo_union_Ioc_eq_Ioc_sdiff_singleton {α : Type u_1} [LinearOrder α] {a b c : α} (a_le_b : a ≤ b) (b_le_c : b ≤ c) :
Ioo a b ∪ Ioc b c = Ioc a c \ {b}

Intersection, difference, complement #

source
@[simp]
theorem Set.Ioi_inter_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a ∩ Ioi b = Ioi (max a b)
source
@[simp]
theorem Set.Iio_inter_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a ∩ Iio b = Iio (min a b)
source
theorem Set.Ico_inter_Ico {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (max a₁ a₂) (min b₁ b₂)
source
theorem Set.Ioc_inter_Ioc {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ioc b₁ a₁ ∩ Ioc b₂ a₂ = Ioc (max b₁ b₂) (min a₁ a₂)
source
theorem Set.Ioo_inter_Ioo {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) (min b₁ b₂)
source
theorem Set.Ioo_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a b ∩ Iio c = Ioo a (min b c)
source
theorem Set.Ioo_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo b a ∩ Ioi c = Ioo (max b c) a
source
theorem Set.Iio_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Iio a ∩ Ioo b c = Ioo b (min a c)
source
theorem Set.Ioi_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioi a ∩ Ioo c b = Ioo (max a c) b
source
theorem Set.Ioc_inter_Ioo_of_left_lt {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₁ < b₂) :
Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁
source
theorem Set.Ioc_inter_Ioo_of_right_le {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₂ ≤ b₁) :
Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂
source
theorem Set.Ioo_inter_Ioc_of_left_le {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₁ ≤ b₂) :
Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁
source
theorem Set.Ioo_inter_Ioc_of_right_lt {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₂ < b₁) :
Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂
source
@[simp]
theorem Set.Ico_sdiff_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a b \ Iio c = Ico (max a c) b
source
@[deprecated Set.Ico_sdiff_Iio (since := "2026-06-03")]
theorem Set.Ico_diff_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a b \ Iio c = Ico (max a c) b

Alias of Set.Ico_sdiff_Iio.

source
@[simp]
theorem Set.Ioc_sdiff_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Ioi c = Ioc a (min b c)
source
@[deprecated Set.Ioc_sdiff_Ioi (since := "2026-06-03")]
theorem Set.Ioc_diff_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Ioi c = Ioc a (min b c)

Alias of Set.Ioc_sdiff_Ioi.

source
@[simp]
theorem Set.Ioc_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b ∩ Ioi c = Ioc (max a c) b
source
@[simp]
theorem Set.Ico_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a b ∩ Iio c = Ico a (min b c)
source
@[simp]
theorem Set.Ioc_sdiff_Iic {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Iic c = Ioc (max a c) b
source
@[deprecated Set.Ioc_sdiff_Iic (since := "2026-06-03")]
theorem Set.Ioc_diff_Iic {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Iic c = Ioc (max a c) b

Alias of Set.Ioc_sdiff_Iic.

source
theorem Set.compl_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
(Ioc a b)ᶜ = Iic a ∪ Ioi b
source
theorem Set.Iic_sdiff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b \ Ioc a b = Iic (min a b)
source
@[deprecated Set.Iic_sdiff_Ioc (since := "2026-06-03")]
theorem Set.Iic_diff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b \ Ioc a b = Iic (min a b)

Alias of Set.Iic_sdiff_Ioc.

source
@[simp]
theorem Set.Ioi_sdiff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ioc a b = Ioi (max a b)
source
@[deprecated Set.Ioi_sdiff_Ioc (since := "2026-06-03")]
theorem Set.Ioi_diff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ioc a b = Ioi (max a b)

Alias of Set.Ioi_sdiff_Ioc.

source
theorem Set.Iic_sdiff_Ioc_self_of_le {α : Type u_1} [LinearOrder α] {a b : α} (hab : a ≤ b) :
Iic b \ Ioc a b = Iic a
source
@[deprecated Set.Iic_sdiff_Ioc_self_of_le (since := "2026-06-03")]
theorem Set.Iic_diff_Ioc_self_of_le {α : Type u_1} [LinearOrder α] {a b : α} (hab : a ≤ b) :
Iic b \ Ioc a b = Iic a

Alias of Set.Iic_sdiff_Ioc_self_of_le.

source
@[simp]
theorem Set.Ioc_union_Ioc_right {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b ∪ Ioc a c = Ioc a (max b c)
source
@[simp]
theorem Set.Ioc_union_Ioc_left {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a c ∪ Ioc b c = Ioc (min a b) c
source
@[simp]
theorem Set.Ioc_union_Ioc_symm {α : Type u_1} [LinearOrder α] {a b : α} :
Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)
source
@[simp]
theorem Set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))