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.

theorem Set.notMem_Ici {α : Type u_1} [LinearOrder α] {a c : α} : c ∉ Ici a ↔ c < a

theorem Set.notMem_Iic {α : Type u_1} [LinearOrder α] {b c : α} : c ∉ Iic b ↔ b < c

theorem Set.notMem_Ioi {α : Type u_1} [LinearOrder α] {a c : α} : c ∉ Ioi a ↔ c ≤ a

theorem Set.notMem_Iio {α : Type u_1} [LinearOrder α] {b c : α} : c ∉ Iio b ↔ b ≤ c

@[simp]

theorem Set.compl_Iic {α : Type u_1} [LinearOrder α] {a : α} : (Iic a)ᶜ = Ioi a

@[simp]

theorem Set.compl_Ici {α : Type u_1} [LinearOrder α] {a : α} : (Ici a)ᶜ = Iio a

@[simp]

theorem Set.compl_Iio {α : Type u_1} [LinearOrder α] {a : α} : (Iio a)ᶜ = Ici a

@[simp]

theorem Set.compl_Ioi {α : Type u_1} [LinearOrder α] {a : α} : (Ioi a)ᶜ = Iic a

@[simp]

theorem Set.Ici_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ici a \ Ici b = Ico a b

@[simp]

theorem Set.Ici_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Ici a \ Ioi b = Icc a b

@[simp]

theorem Set.Ioi_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a \ Ioi b = Ioc a b

@[simp]

theorem Set.Ioi_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a \ Ici b = Ioo a b

@[simp]

theorem Set.Iic_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} : Iic b \ Iic a = Ioc a b

@[simp]

theorem Set.Iio_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} : Iio b \ Iic a = Ioo a b

@[simp]

theorem Set.Iic_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Iic b \ Iio a = Icc a b

@[simp]

theorem Set.Iio_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Iio b \ Iio a = Ico a b

theorem Set.Ioi_injective {α : Type u_1} [LinearOrder α] : Function.Injective Ioi

theorem Set.Iio_injective {α : Type u_1} [LinearOrder α] : Function.Injective Iio

theorem Set.Ioi_inj {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a = Ioi b ↔ a = b

theorem Set.Iio_inj {α : Type u_1} [LinearOrder α] {a b : α} : Iio a = Iio b ↔ a = b

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₂

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₁

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

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

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₂

theorem Set.Ici_eq_singleton_iff_isTop {α : Type u_1} [LinearOrder α] {x : α} : Ici x = {x} ↔ IsTop x

@[simp]

theorem Set.Ioi_subset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} : Ioi b ⊆ Ioi a ↔ a ≤ b

@[simp]

theorem Set.Ioi_ssubset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} : Ioi b ⊂ Ioi a ↔ a < b

@[simp]

theorem Set.Ioi_subset_Ici_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] : Ioi b ⊆ Ici a ↔ a ≤ b

@[simp]

theorem Set.Iio_subset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} : Iio a ⊆ Iio b ↔ a ≤ b

@[simp]

theorem Set.Iio_ssubset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} : Iio a ⊂ Iio b ↔ a < b

@[simp]

theorem Set.Iio_subset_Iic_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] : Iio a ⊆ Iic b ↔ a ≤ b

Two infinite intervals

theorem Set.Iic_union_Ioi_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iic b ∪ Ioi a = univ

theorem Set.Iio_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iio b ∪ Ici a = univ

theorem Set.Iic_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iic b ∪ Ici a = univ

theorem Set.Iio_union_Ioi_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Iio b ∪ Ioi a = univ

@[simp]

theorem Set.Iic_union_Ici {α : Type u_1} [LinearOrder α] {a : α} : Iic a ∪ Ici a = univ

@[simp]

theorem Set.Iio_union_Ici {α : Type u_1} [LinearOrder α] {a : α} : Iio a ∪ Ici a = univ

@[simp]

theorem Set.Iic_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} : Iic a ∪ Ioi a = univ

@[simp]

theorem Set.Iio_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} : Iio a ∪ Ioi a = {a}ᶜ

A finite and an infinite interval

theorem Set.Ioo_union_Ioi' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c < b) : Ioo a b ∪ Ioi c = Ioi (min a c)

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)

theorem Set.Ioi_subset_Ioo_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a ⊆ Ioo a b ∪ Ici b

@[simp]

theorem Set.Ioo_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Ioo a b ∪ Ici b = Ioi a

theorem Set.Ici_subset_Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ici a ⊆ Ico a b ∪ Ici b

@[simp]

theorem Set.Ico_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Ico a b ∪ Ici b = Ici a

theorem Set.Ico_union_Ici' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Ico a b ∪ Ici c = Ici (min a c)

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)

theorem Set.Ioi_subset_Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a ⊆ Ioc a b ∪ Ioi b

@[simp]

theorem Set.Ioc_union_Ioi_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Ioc a b ∪ Ioi b = Ioi a

theorem Set.Ioc_union_Ioi' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Ioc a b ∪ Ioi c = Ioi (min a c)

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)

theorem Set.Ici_subset_Icc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Ici a ⊆ Icc a b ∪ Ioi b

@[simp]

theorem Set.Icc_union_Ioi_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Icc a b ∪ Ioi b = Ici a

theorem Set.Ioi_subset_Ioc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a ⊆ Ioc a b ∪ Ici b

@[simp]

theorem Set.Ioc_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Ioc a b ∪ Ici b = Ioi a

theorem Set.Ici_subset_Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Ici a ⊆ Icc a b ∪ Ici b

@[simp]

theorem Set.Icc_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Icc a b ∪ Ici b = Ici a

theorem Set.Icc_union_Ici' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Icc a b ∪ Ici c = Ici (min a c)

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)

An infinite and a finite interval

theorem Set.Iic_subset_Iio_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} : Iic b ⊆ Iio a ∪ Icc a b

@[simp]

theorem Set.Iio_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iio a ∪ Icc a b = Iic b

theorem Set.Iio_subset_Iio_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} : Iio b ⊆ Iio a ∪ Ico a b

@[simp]

theorem Set.Iio_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iio a ∪ Ico a b = Iio b

theorem Set.Iio_union_Ico' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c ≤ b) : Iio b ∪ Ico c d = Iio (max b d)

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)

theorem Set.Iic_subset_Iic_union_Ioc {α : Type u_1} [LinearOrder α] {a b : α} : Iic b ⊆ Iic a ∪ Ioc a b

@[simp]

theorem Set.Iic_union_Ioc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iic a ∪ Ioc a b = Iic b

theorem Set.Iic_union_Ioc' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c < b) : Iic b ∪ Ioc c d = Iic (max b d)

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)

theorem Set.Iio_subset_Iic_union_Ioo {α : Type u_1} [LinearOrder α] {a b : α} : Iio b ⊆ Iic a ∪ Ioo a b

@[simp]

theorem Set.Iic_union_Ioo_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Iic a ∪ Ioo a b = Iio b

theorem Set.Iio_union_Ioo' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c < b) : Iio b ∪ Ioo c d = Iio (max b d)

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)

theorem Set.Iic_subset_Iic_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} : Iic b ⊆ Iic a ∪ Icc a b

@[simp]

theorem Set.Iic_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Iic a ∪ Icc a b = Iic b

theorem Set.Iic_union_Icc' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c ≤ b) : Iic b ∪ Icc c d = Iic (max b d)

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)

theorem Set.Iio_subset_Iic_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} : Iio b ⊆ Iic a ∪ Ico a b

@[simp]

theorem Set.Iic_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Iic a ∪ Ico a b = Iio b

Two finite intervals, I?o and Ic?

theorem Set.Ioo_subset_Ioo_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} : Ioo a c ⊆ Ioo a b ∪ Ico b c

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

theorem Set.Ico_subset_Ico_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} : Ico a c ⊆ Ico a b ∪ Ico b c

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

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)

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)

theorem Set.Icc_subset_Ico_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} : Icc a c ⊆ Ico a b ∪ Icc b c

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

theorem Set.Ioc_subset_Ioo_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a c ⊆ Ioo a b ∪ Icc b c

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

theorem Set.Ioo_subset_Ioc_union_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Ioo a c ⊆ Ioc a b ∪ Ioo b c

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

theorem Set.Ico_subset_Icc_union_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Ico a c ⊆ Icc a b ∪ Ioo b c

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

theorem Set.Icc_subset_Icc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} : Icc a c ⊆ Icc a b ∪ Ioc b c

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

theorem Set.Ioc_subset_Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a c ⊆ Ioc a b ∪ Ioc b c

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

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)

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)

Two finite intervals with a common point

theorem Set.Ioo_subset_Ioc_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} : Ioo a c ⊆ Ioc a b ∪ Ico b c

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

theorem Set.Ico_subset_Icc_union_Ico {α : Type u_1} [LinearOrder α] {a b c : α} : Ico a c ⊆ Icc a b ∪ Ico b c

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

theorem Set.Icc_subset_Icc_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} : Icc a c ⊆ Icc a b ∪ Icc b c

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

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)

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

theorem Set.Ioc_subset_Ioc_union_Icc {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a c ⊆ Ioc a b ∪ Icc b c

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

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)

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)

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

Intersection, difference, complement

@[simp]

theorem Set.Ioi_inter_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Ioi a ∩ Ioi b = Ioi (max a b)

@[simp]

theorem Set.Iio_inter_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Iio a ∩ Iio b = Iio (min a b)

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

theorem Set.Ioc_inter_Ioc {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) (min b₁ b₂)

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

theorem Set.Ioo_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Ioo a b ∩ Iio c = Ioo a (min b c)

theorem Set.Iio_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Iio a ∩ Ioo b c = Ioo b (min a c)

theorem Set.Ioo_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Ioo a b ∩ Ioi c = Ioo (max a c) b

theorem Set.Ioi_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Ioi a ∩ Ioo b c = Ioo (max a b) c

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₁

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₂

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₁

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₂

@[simp]

theorem Set.Ico_diff_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Ico a b \ Iio c = Ico (max a c) b

@[simp]

theorem Set.Ioc_diff_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a b \ Ioi c = Ioc a (min b c)

@[simp]

theorem Set.Ioc_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a b ∩ Ioi c = Ioc (max a c) b

@[simp]

theorem Set.Ico_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Ico a b ∩ Iio c = Ico a (min b c)

@[simp]

theorem Set.Ioc_diff_Iic {α : Type u_1} [LinearOrder α] {a b c : α} : Ioc a b \ Iic c = Ioc (max a c) b

theorem Set.compl_Ioc {α : Type u_1} [LinearOrder α] {a b : α} : (Ioc a b)ᶜ = Iic a ∪ Ioi b

theorem Set.Iic_diff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} : Iic b \ Ioc a b = Iic (min a b)

theorem Set.Iic_diff_Ioc_self_of_le {α : Type u_1} [LinearOrder α] {a b : α} (hab : a ≤ b) : Iic b \ Ioc a b = Iic a

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

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

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

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