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.not_mem_Ici {α : Type u_1} [LinearOrder α] {a c : α} :
c ∉ Ici a ↔ c < a
source
theorem Set.not_mem_Iic {α : Type u_1} [LinearOrder α] {b c : α} :
c ∉ Iic b ↔ b < c
source
theorem Set.not_mem_Ioi {α : Type u_1} [LinearOrder α] {a c : α} :
c ∉ Ioi a ↔ c ≤ a
source
theorem Set.not_mem_Iio {α : Type u_1} [LinearOrder α] {b c : α} :
c ∉ Iio b ↔ b ≤ 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_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ici b = Ico a b
source
@[simp]
theorem Set.Ici_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ici a \ Ioi b = Icc a b
source
@[simp]
theorem Set.Ioi_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ioi b = Ioc a b
source
@[simp]
theorem Set.Ioi_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a \ Ici b = Ioo a b
source
@[simp]
theorem Set.Iic_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b \ Iic a = Ioc a b
source
@[simp]
theorem Set.Iio_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b \ Iic a = Ioo a b
source
@[simp]
theorem Set.Iic_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b \ Iio a = Icc a b
source
@[simp]
theorem Set.Iio_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iio b \ Iio a = Ico a b
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.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.Ico_eq_Ico_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : a₁ < b₁ ∨ a₂ < b₂) :
Ico a₁ b₁ = Ico 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
@[simp]
theorem Set.Ioi_subset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi b ⊆ Ioi a ↔ a ≤ b
source
@[simp]
theorem Set.Ioi_ssubset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi b ⊂ Ioi a ↔ a < b
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_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a ⊆ Iio b ↔ a ≤ b
source
@[simp]
theorem Set.Iio_ssubset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a ⊂ Iio b ↔ a < b
source
@[simp]
theorem Set.Iio_subset_Iic_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] :
Iio a ⊆ Iic b ↔ a ≤ b

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.Iio_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
Iio b ∪ Ici 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.Iio_union_Ioi_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
Iio b ∪ Ioi a = univ
source
@[simp]
theorem Set.Iic_union_Ici {α : Type u_1} [LinearOrder α] {a : α} :
Iic a ∪ Ici a = univ
source
@[simp]
theorem Set.Iio_union_Ici {α : Type u_1} [LinearOrder α] {a : α} :
Iio a ∪ Ici a = univ
source
@[simp]
theorem Set.Iic_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} :
Iic a ∪ Ioi a = univ
source
@[simp]
theorem Set.Iio_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} :
Iio a ∪ Ioi a = {a}ᶜ

A finite and an infinite interval #

source
theorem Set.Ioo_union_Ioi' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c < b) :
Ioo a b ∪ Ioi c = Ioi (a ⊓ c)
source
theorem Set.Ioo_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c < a ⊔ b) :
Ioo a b ∪ Ioi c = Ioi (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 ≤ b) :
Ico a b ∪ Ici c = Ici (a ⊓ c)
source
theorem Set.Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) :
Ico a b ∪ Ici c = Ici (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 ≤ b) :
Ioc a b ∪ Ioi c = Ioi (a ⊓ c)
source
theorem Set.Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) :
Ioc a b ∪ Ioi c = Ioi (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 ≤ b) :
Icc a b ∪ Ici c = Ici (a ⊓ c)
source
theorem Set.Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) :
Icc a b ∪ Ici c = Ici (a ⊓ c)

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₁ : c ≤ b) :
Iio b ∪ Ico c d = Iio (b ⊔ d)
source
theorem Set.Iio_union_Ico {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d ≤ b) :
Iio b ∪ Ico c d = Iio (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₁ : c < b) :
Iic b ∪ Ioc c d = Iic (b ⊔ d)
source
theorem Set.Iic_union_Ioc {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d < b) :
Iic b ∪ Ioc c d = Iic (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₁ : c < b) :
Iio b ∪ Ioo c d = Iio (b ⊔ d)
source
theorem Set.Iio_union_Ioo {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d < b) :
Iio b ∪ Ioo c d = Iio (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₁ : c ≤ b) :
Iic b ∪ Icc c d = Iic (b ⊔ d)
source
theorem Set.Iic_union_Icc {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d ≤ b) :
Iic b ∪ Icc c d = Iic (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

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₁ : c ≤ b) (h₂ : a ≤ d) :
Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)
source
theorem Set.Ico_union_Ico {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b ≤ c ⊔ d) (h₂ : c ⊓ d ≤ a ⊔ b) :
Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)
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₁ : c ≤ b) (h₂ : a ≤ d) :
Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)
source
theorem Set.Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b ≤ c ⊔ d) (h₂ : c ⊓ d ≤ a ⊔ b) :
Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

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
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 (a ⊓ c) (b ⊔ d)
source
theorem Set.Icc_union_Icc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b < c ⊔ d) (h₂ : c ⊓ d < a ⊔ b) :
Icc a b ∪ Icc c d = Icc (a ⊓ c) (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 (a ⊓ c) (b ⊔ d)
source
theorem Set.Ioo_union_Ioo {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b < c ⊔ d) (h₂ : c ⊓ d < a ⊔ b) :
Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (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

Intersection, difference, complement #

source
@[simp]
theorem Set.Ioi_inter_Ioi {α : Type u_1} [LinearOrder α] {a b : α} :
Ioi a ∩ Ioi b = Ioi (a ⊔ b)
source
@[simp]
theorem Set.Iio_inter_Iio {α : Type u_1} [LinearOrder α] {a b : α} :
Iio a ∩ Iio b = Iio (a ⊓ b)
source
theorem Set.Ico_inter_Ico {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
source
theorem Set.Ioc_inter_Ioc {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ioc a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
source
theorem Set.Ioo_inter_Ioo {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)
source
theorem Set.Ioo_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a b ∩ Iio c = Ioo a (b ⊓ c)
source
theorem Set.Iio_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Iio a ∩ Ioo b c = Ioo b (a ⊓ c)
source
theorem Set.Ioo_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioo a b ∩ Ioi c = Ioo (a ⊔ c) b
source
theorem Set.Ioi_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioi a ∩ Ioo b c = Ioo (a ⊔ b) c
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 (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 (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 (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 (a₁ ⊔ a₂) b₂
source
@[simp]
theorem Set.Ico_diff_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a b \ Iio c = Ico (a ⊔ c) b
source
@[simp]
theorem Set.Ioc_diff_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Ioi c = Ioc a (b ⊓ c)
source
@[simp]
theorem Set.Ioc_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b ∩ Ioi c = Ioc (a ⊔ c) b
source
@[simp]
theorem Set.Ico_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} :
Ico a b ∩ Iio c = Ico a (b ⊓ c)
source
@[simp]
theorem Set.Ioc_diff_Iic {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b \ Iic c = Ioc (a ⊔ c) b
source
theorem Set.compl_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
(Ioc a b)ᶜ = Iic a ∪ Ioi b
source
theorem Set.Iic_diff_Ioc {α : Type u_1} [LinearOrder α] {a b : α} :
Iic b \ Ioc a b = Iic (a ⊓ b)
source
theorem Set.Iic_diff_Ioc_self_of_le {α : Type u_1} [LinearOrder α] {a b : α} (hab : a ≤ b) :
Iic b \ Ioc a b = Iic a
source
@[simp]
theorem Set.Ioc_union_Ioc_right {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a b ∪ Ioc a c = Ioc a (b ⊔ c)
source
@[simp]
theorem Set.Ioc_union_Ioc_left {α : Type u_1} [LinearOrder α] {a b c : α} :
Ioc a c ∪ Ioc b c = Ioc (a ⊓ b) c
source
@[simp]
theorem Set.Ioc_union_Ioc_symm {α : Type u_1} [LinearOrder α] {a b : α} :
Ioc a b ∪ Ioc b a = Ioc (a ⊓ b) (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 (a ⊓ (b ⊓ c)) (a ⊔ (b ⊔ c))