mathlib documentation

data.set.intervals.basic

Intervals

In any preorder α, we define intervals (which on each side can be either infinite, open, or closed) using the following naming conventions:

Each interval has the name I + letter for left side + letter for right side. For instance, Ioc a b denotes the inverval (a, b].

This file contains these definitions, and basic facts on inclusion, intersection, difference of intervals (where the precise statements may depend on the properties of the order, in particular for some statements it should be linear_order or densely_ordered).

TODO: This is just the beginning; a lot of rules are missing

def set.Ioo {α : Type u} [preorder α] :
α → α → set α

Left-open right-open interval

Equations
def set.Ico {α : Type u} [preorder α] :
α → α → set α

Left-closed right-open interval

Equations
def set.Iio {α : Type u} [preorder α] :
α → set α

Left-infinite right-open interval

Equations
def set.Icc {α : Type u} [preorder α] :
α → α → set α

Left-closed right-closed interval

Equations
def set.Iic {α : Type u} [preorder α] :
α → set α

Left-infinite right-closed interval

Equations
def set.Ioc {α : Type u} [preorder α] :
α → α → set α

Left-open right-closed interval

Equations
def set.Ici {α : Type u} [preorder α] :
α → set α

Left-closed right-infinite interval

Equations
def set.Ioi {α : Type u} [preorder α] :
α → set α

Left-open right-infinite interval

Equations
theorem set.Ioo_def {α : Type u} [preorder α] (a b : α) :
{x : α | a < x x < b} = set.Ioo a b

theorem set.Ico_def {α : Type u} [preorder α] (a b : α) :
{x : α | a x x < b} = set.Ico a b

theorem set.Iio_def {α : Type u} [preorder α] (a : α) :
{x : α | x < a} = set.Iio a

theorem set.Icc_def {α : Type u} [preorder α] (a b : α) :
{x : α | a x x b} = set.Icc a b

theorem set.Iic_def {α : Type u} [preorder α] (b : α) :
{x : α | x b} = set.Iic b

theorem set.Ioc_def {α : Type u} [preorder α] (a b : α) :
{x : α | a < x x b} = set.Ioc a b

theorem set.Ici_def {α : Type u} [preorder α] (a : α) :
{x : α | a x} = set.Ici a

theorem set.Ioi_def {α : Type u} [preorder α] (a : α) :
{x : α | a < x} = set.Ioi a

@[simp]
theorem set.mem_Ioo {α : Type u} [preorder α] {a b x : α} :
x set.Ioo a b a < x x < b

@[simp]
theorem set.mem_Ico {α : Type u} [preorder α] {a b x : α} :
x set.Ico a b a x x < b

@[simp]
theorem set.mem_Iio {α : Type u} [preorder α] {b x : α} :
x set.Iio b x < b

@[simp]
theorem set.mem_Icc {α : Type u} [preorder α] {a b x : α} :
x set.Icc a b a x x b

@[simp]
theorem set.mem_Iic {α : Type u} [preorder α] {b x : α} :
x set.Iic b x b

@[simp]
theorem set.mem_Ioc {α : Type u} [preorder α] {a b x : α} :
x set.Ioc a b a < x x b

@[simp]
theorem set.mem_Ici {α : Type u} [preorder α] {a x : α} :
x set.Ici a a x

@[simp]
theorem set.mem_Ioi {α : Type u} [preorder α] {a x : α} :
x set.Ioi a a < x

@[simp]
theorem set.left_mem_Ioo {α : Type u} [preorder α] {a b : α} :

@[simp]
theorem set.left_mem_Ico {α : Type u} [preorder α] {a b : α} :
a set.Ico a b a < b

@[simp]
theorem set.left_mem_Icc {α : Type u} [preorder α] {a b : α} :
a set.Icc a b a b

@[simp]
theorem set.left_mem_Ioc {α : Type u} [preorder α] {a b : α} :

theorem set.left_mem_Ici {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.right_mem_Ioo {α : Type u} [preorder α] {a b : α} :

@[simp]
theorem set.right_mem_Ico {α : Type u} [preorder α] {a b : α} :

@[simp]
theorem set.right_mem_Icc {α : Type u} [preorder α] {a b : α} :
b set.Icc a b a b

@[simp]
theorem set.right_mem_Ioc {α : Type u} [preorder α] {a b : α} :
b set.Ioc a b a < b

theorem set.right_mem_Iic {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.dual_Ici {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.dual_Iic {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.dual_Ioi {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.dual_Iio {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.dual_Icc {α : Type u} [preorder α] {a b : α} :
set.Icc a b = set.Icc b a

@[simp]
theorem set.dual_Ioc {α : Type u} [preorder α] {a b : α} :
set.Ioc a b = set.Ico b a

@[simp]
theorem set.dual_Ico {α : Type u} [preorder α] {a b : α} :
set.Ico a b = set.Ioc b a

@[simp]
theorem set.dual_Ioo {α : Type u} [preorder α] {a b : α} :
set.Ioo a b = set.Ioo b a

@[simp]
theorem set.nonempty_Icc {α : Type u} [preorder α] {a b : α} :

@[simp]
theorem set.nonempty_Ico {α : Type u} [preorder α] {a b : α} :
(set.Ico a b).nonempty a < b

@[simp]
theorem set.nonempty_Ioc {α : Type u} [preorder α] {a b : α} :
(set.Ioc a b).nonempty a < b

@[simp]
theorem set.nonempty_Ici {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.nonempty_Iic {α : Type u} [preorder α] {a : α} :

@[simp]
theorem set.nonempty_Ioo {α : Type u} [preorder α] {a b : α} [densely_ordered α] :
(set.Ioo a b).nonempty a < b

@[simp]
theorem set.nonempty_Ioi {α : Type u} [preorder α] {a : α} [no_top_order α] :

@[simp]
theorem set.nonempty_Iio {α : Type u} [preorder α] {a : α} [no_bot_order α] :

theorem set.nonempty_Icc_subtype {α : Type u} [preorder α] {a b : α} :
a bnonempty (set.Icc a b)

theorem set.nonempty_Ico_subtype {α : Type u} [preorder α] {a b : α} :
a < bnonempty (set.Ico a b)

theorem set.nonempty_Ioc_subtype {α : Type u} [preorder α] {a b : α} :
a < bnonempty (set.Ioc a b)

@[instance]
def set.nonempty_Ici_subtype {α : Type u} [preorder α] {a : α} :

An interval Ici a is nonempty.

@[instance]
def set.nonempty_Iic_subtype {α : Type u} [preorder α] {a : α} :

An interval Iic a is nonempty.

theorem set.nonempty_Ioo_subtype {α : Type u} [preorder α] {a b : α} [densely_ordered α] :
a < bnonempty (set.Ioo a b)

@[instance]
def set.nonempty_Ioi_subtype {α : Type u} [preorder α] {a : α} [no_top_order α] :

In a no_top_order, the intervals Ioi are nonempty.

@[instance]
def set.nonempty_Iio_subtype {α : Type u} [preorder α] {a : α} [no_bot_order α] :

In a no_bot_order, the intervals Iio are nonempty.

@[simp]
theorem set.Ioo_eq_empty {α : Type u} [preorder α] {a b : α} :
b aset.Ioo a b =

@[simp]
theorem set.Ico_eq_empty {α : Type u} [preorder α] {a b : α} :
b aset.Ico a b =

@[simp]
theorem set.Icc_eq_empty {α : Type u} [preorder α] {a b : α} :
b < aset.Icc a b =

@[simp]
theorem set.Ioc_eq_empty {α : Type u} [preorder α] {a b : α} :
b aset.Ioc a b =

@[simp]
theorem set.Ioo_self {α : Type u} [preorder α] (a : α) :

@[simp]
theorem set.Ico_self {α : Type u} [preorder α] (a : α) :

@[simp]
theorem set.Ioc_self {α : Type u} [preorder α] (a : α) :

theorem set.Ici_subset_Ici {α : Type u} [preorder α] {a b : α} :

theorem set.Iic_subset_Iic {α : Type u} [preorder α] {a b : α} :

theorem set.Ici_subset_Ioi {α : Type u} [preorder α] {a b : α} :

theorem set.Iic_subset_Iio {α : Type u} [preorder α] {a b : α} :

theorem set.Ioo_subset_Ioo {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₂ a₁b₁ b₂set.Ioo a₁ b₁ set.Ioo a₂ b₂

theorem set.Ioo_subset_Ioo_left {α : Type u} [preorder α] {a₁ a₂ b : α} :
a₁ a₂set.Ioo a₂ b set.Ioo a₁ b

theorem set.Ioo_subset_Ioo_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ b₂set.Ioo a b₁ set.Ioo a b₂

theorem set.Ico_subset_Ico {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₂ a₁b₁ b₂set.Ico a₁ b₁ set.Ico a₂ b₂

theorem set.Ico_subset_Ico_left {α : Type u} [preorder α] {a₁ a₂ b : α} :
a₁ a₂set.Ico a₂ b set.Ico a₁ b

theorem set.Ico_subset_Ico_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ b₂set.Ico a b₁ set.Ico a b₂

theorem set.Icc_subset_Icc {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₂ a₁b₁ b₂set.Icc a₁ b₁ set.Icc a₂ b₂

theorem set.Icc_subset_Icc_left {α : Type u} [preorder α] {a₁ a₂ b : α} :
a₁ a₂set.Icc a₂ b set.Icc a₁ b

theorem set.Icc_subset_Icc_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ b₂set.Icc a b₁ set.Icc a b₂

theorem set.Icc_subset_Ioo {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₂ < a₁b₁ < b₂set.Icc a₁ b₁ set.Ioo a₂ b₂

theorem set.Icc_subset_Ici_self {α : Type u} [preorder α] {a b : α} :

theorem set.Icc_subset_Iic_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioc_subset_Iic_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioc_subset_Ioc {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₂ a₁b₁ b₂set.Ioc a₁ b₁ set.Ioc a₂ b₂

theorem set.Ioc_subset_Ioc_left {α : Type u} [preorder α] {a₁ a₂ b : α} :
a₁ a₂set.Ioc a₂ b set.Ioc a₁ b

theorem set.Ioc_subset_Ioc_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ b₂set.Ioc a b₁ set.Ioc a b₂

theorem set.Ico_subset_Ioo_left {α : Type u} [preorder α] {a₁ a₂ b : α} :
a₁ < a₂set.Ico a₂ b set.Ioo a₁ b

theorem set.Ioc_subset_Ioo_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ < b₂set.Ioc a b₁ set.Ioo a b₂

theorem set.Icc_subset_Ico_right {α : Type u} [preorder α] {a b₁ b₂ : α} :
b₁ < b₂set.Icc a b₁ set.Ico a b₂

theorem set.Ioo_subset_Ico_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioo_subset_Ioc_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ico_subset_Icc_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioc_subset_Icc_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioo_subset_Icc_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ico_subset_Iio_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioo_subset_Iio_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioc_subset_Ioi_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioo_subset_Ioi_self {α : Type u} [preorder α] {a b : α} :

theorem set.Ioi_subset_Ici_self {α : Type u} [preorder α] {a : α} :

theorem set.Iio_subset_Iic_self {α : Type u} [preorder α] {a : α} :

theorem set.Ico_subset_Ici_self {α : Type u} [preorder α] {a b : α} :

theorem set.Icc_subset_Icc_iff {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Icc a₂ b₂ a₂ a₁ b₁ b₂)

theorem set.Icc_subset_Ioo_iff {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Ioo a₂ b₂ a₂ < a₁ b₁ < b₂)

theorem set.Icc_subset_Ico_iff {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Ico a₂ b₂ a₂ a₁ b₁ < b₂)

theorem set.Icc_subset_Ioc_iff {α : Type u} [preorder α] {a₁ a₂ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Ioc a₂ b₂ a₂ < a₁ b₁ b₂)

theorem set.Icc_subset_Iio_iff {α : Type u} [preorder α] {a₁ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Iio b₂ b₁ < b₂)

theorem set.Icc_subset_Ioi_iff {α : Type u} [preorder α] {a₁ a₂ b₁ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Ioi a₂ a₂ < a₁)

theorem set.Icc_subset_Iic_iff {α : Type u} [preorder α] {a₁ b₁ b₂ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Iic b₂ b₁ b₂)

theorem set.Icc_subset_Ici_iff {α : Type u} [preorder α] {a₁ a₂ b₁ : α} :
a₁ b₁(set.Icc a₁ b₁ set.Ici a₂ a₂ a₁)

theorem set.Ioi_subset_Ioi {α : Type u} [preorder α] {a b : α} :
a bset.Ioi b set.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_subset_Ici {α : Type u} [preorder α] {a b : α} :
a bset.Ioi b set.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} [preorder α] {a b : α} :
a bset.Iio a set.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_subset_Iic {α : Type u} [preorder α] {a b : α} :
a bset.Iio a set.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} [preorder α] {a b : α} :

theorem set.Ici_inter_Iio {α : Type u} [preorder α] {a b : α} :

theorem set.Ioi_inter_Iic {α : Type u} [preorder α] {a b : α} :

theorem set.Ioi_inter_Iio {α : Type u} [preorder α] {a b : α} :

@[simp]
theorem set.Icc_self {α : Type u} [partial_order α] (a : α) :
set.Icc a a = {a}

@[simp]
theorem set.Icc_diff_left {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {a} = set.Ioc a b

@[simp]
theorem set.Icc_diff_right {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {b} = set.Ico a b

@[simp]
theorem set.Ico_diff_left {α : Type u} [partial_order α] {a b : α} :
set.Ico a b \ {a} = set.Ioo a b

@[simp]
theorem set.Ioc_diff_right {α : Type u} [partial_order α] {a b : α} :
set.Ioc a b \ {b} = set.Ioo a b

@[simp]
theorem set.Icc_diff_both {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {a, b} = set.Ioo a b

@[simp]
theorem set.Ici_diff_left {α : Type u} [partial_order α] {a : α} :
set.Ici a \ {a} = set.Ioi a

@[simp]
theorem set.Iic_diff_right {α : Type u} [partial_order α] {a : α} :
set.Iic a \ {a} = set.Iio a

@[simp]
theorem set.Ico_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :
a < bset.Ico a b \ set.Ioo a b = {a}

@[simp]
theorem set.Ioc_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :
a < bset.Ioc a b \ set.Ioo a b = {b}

@[simp]
theorem set.Icc_diff_Ico_same {α : Type u} [partial_order α] {a b : α} :
a bset.Icc a b \ set.Ico a b = {b}

@[simp]
theorem set.Icc_diff_Ioc_same {α : Type u} [partial_order α] {a b : α} :
a bset.Icc a b \ set.Ioc a b = {a}

@[simp]
theorem set.Icc_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :
a bset.Icc a b \ set.Ioo a b = {a, b}

@[simp]
theorem set.Ici_diff_Ioi_same {α : Type u} [partial_order α] {a : α} :
set.Ici a \ set.Ioi a = {a}

@[simp]
theorem set.Iic_diff_Iio_same {α : Type u} [partial_order α] {a : α} :
set.Iic a \ set.Iio a = {a}

@[simp]
theorem set.Ioi_union_left {α : Type u} [partial_order α] {a : α} :

@[simp]
theorem set.Iio_union_right {α : Type u} [partial_order α] {a : α} :

theorem set.Ioo_union_left {α : Type u} [partial_order α] {a b : α} :
a < bset.Ioo a b {a} = set.Ico a b

theorem set.Ioo_union_right {α : Type u} [partial_order α] {a b : α} :
a < bset.Ioo a b {b} = set.Ioc a b

theorem set.Ioc_union_left {α : Type u} [partial_order α] {a b : α} :
a bset.Ioc a b {a} = set.Icc a b

theorem set.Ico_union_right {α : Type u} [partial_order α] {a b : α} :
a bset.Ico a b {b} = set.Icc a b

theorem set.mem_Ici_Ioi_of_subset_of_subset {α : Type u} [partial_order α] {a : α} {s : set α} :
set.Ioi a ss set.Ici as {set.Ici a, set.Ioi a}

theorem set.mem_Iic_Iio_of_subset_of_subset {α : Type u} [partial_order α] {a : α} {s : set α} :
set.Iio a ss set.Iic as {set.Iic a, set.Iio a}

theorem set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u} [partial_order α] {a b : α} {s : set α} :
set.Ioo a b ss set.Icc a bs {set.Icc a b, set.Ico a b, set.Ioc a b, set.Ioo a b}

theorem set.mem_Ioo_or_eq_endpoints_of_mem_Icc {α : Type u} [partial_order α] {a b x : α} :
x set.Icc a bx = a x = b x set.Ioo a b

theorem set.mem_Ioo_or_eq_left_of_mem_Ico {α : Type u} [partial_order α] {a b x : α} :
x set.Ico a bx = a x set.Ioo a b

theorem set.mem_Ioo_or_eq_right_of_mem_Ioc {α : Type u} [partial_order α] {a b x : α} :
x set.Ioc a bx = b x set.Ioo a b

theorem set.Ici_singleton_of_top {α : Type u} [partial_order α] {a : α} :
(∀ (x : α), x a)set.Ici a = {a}

theorem set.Iic_singleton_of_bot {α : Type u} [partial_order α] {a : α} :
(∀ (x : α), a x)set.Iic a = {a}

@[simp]
theorem set.Ici_top {α : Type u} [order_top α] :

@[simp]
theorem set.Iic_top {α : Type u} [order_top α] :

@[simp]
theorem set.Icc_top {α : Type u} [order_top α] {a : α} :

@[simp]
theorem set.Ioc_top {α : Type u} [order_top α] {a : α} :

@[simp]
theorem set.Iic_bot {α : Type u} [order_bot α] :

@[simp]
theorem set.Ici_bot {α : Type u} [order_bot α] :

@[simp]
theorem set.Icc_bot {α : Type u} [order_bot α] {a : α} :

@[simp]
theorem set.Ico_bot {α : Type u} [order_bot α] {a : α} :

@[simp]
theorem set.compl_Iic {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.compl_Ici {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.compl_Iio {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.compl_Ioi {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.Ici_diff_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ici_diff_Ioi {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioi_diff_Ioi {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioi_diff_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_diff_Iic {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iio_diff_Iic {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_diff_Iio {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iio_diff_Iio {α : Type u} [linear_order α] {a b : α} :

theorem set.Ioo_eq_empty_iff {α : Type u} [linear_order α] {a b : α} [densely_ordered α] :
set.Ioo a b = b a

theorem set.Ico_eq_empty_iff {α : Type u} [linear_order α] {a b : α} :
set.Ico a b = b a

theorem set.Icc_eq_empty_iff {α : Type u} [linear_order α] {a b : α} :
set.Icc a b = b < a

theorem set.Ico_subset_Ico_iff {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
a₁ < b₁(set.Ico a₁ b₁ set.Ico a₂ b₂ a₂ a₁ b₁ b₂)

theorem set.Ioo_subset_Ioo_iff {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} [densely_ordered α] :
a₁ < b₁(set.Ioo a₁ b₁ set.Ioo a₂ b₂ a₂ a₁ b₁ b₂)

theorem set.Ico_eq_Ico_iff {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
a₁ < b₁ a₂ < b₂(set.Ico a₁ b₁ = set.Ico a₂ b₂ a₁ = a₂ b₁ = b₂)

@[simp]
theorem set.Ioi_subset_Ioi_iff {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioi_subset_Ici_iff {α : Type u} [linear_order α] {a b : α} [densely_ordered α] :

@[simp]
theorem set.Iio_subset_Iio_iff {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iio_subset_Iic_iff {α : Type u} [linear_order α] {a b : α} [densely_ordered α] :

Unions of adjacent intervals

Two infinite intervals

@[simp]
theorem set.Iic_union_Ici {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.Iio_union_Ici {α : Type u} [linear_order α] {a : α} :

@[simp]
theorem set.Iic_union_Ioi {α : Type u} [linear_order α] {a : α} :

A finite and an infinite interval

theorem set.Ioi_subset_Ioo_union_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioo_union_Ici_eq_Ioi {α : Type u} [linear_order α] {a b : α} :
a < bset.Ioo a b set.Ici b = set.Ioi a

theorem set.Ici_subset_Ico_union_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ico_union_Ici_eq_Ici {α : Type u} [linear_order α] {a b : α} :
a bset.Ico a b set.Ici b = set.Ici a

theorem set.Ioi_subset_Ioc_union_Ioi {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioc_union_Ioi_eq_Ioi {α : Type u} [linear_order α] {a b : α} :
a bset.Ioc a b set.Ioi b = set.Ioi a

theorem set.Ici_subset_Icc_union_Ioi {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Icc_union_Ioi_eq_Ici {α : Type u} [linear_order α] {a b : α} :
a bset.Icc a b set.Ioi b = set.Ici a

theorem set.Ioi_subset_Ioc_union_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Ioc_union_Ici_eq_Ioi {α : Type u} [linear_order α] {a b : α} :
a < bset.Ioc a b set.Ici b = set.Ioi a

theorem set.Ici_subset_Icc_union_Ici {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Icc_union_Ici_eq_Ici {α : Type u} [linear_order α] {a b : α} :
a bset.Icc a b set.Ici b = set.Ici a

An infinite and a finite interval

theorem set.Iic_subset_Iio_union_Icc {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iio_union_Icc_eq_Iic {α : Type u} [linear_order α] {a b : α} :
a bset.Iio a set.Icc a b = set.Iic b

theorem set.Iio_subset_Iio_union_Ico {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iio_union_Ico_eq_Iio {α : Type u} [linear_order α] {a b : α} :
a bset.Iio a set.Ico a b = set.Iio b

theorem set.Iic_subset_Iic_union_Ioc {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_union_Ioc_eq_Iic {α : Type u} [linear_order α] {a b : α} :
a bset.Iic a set.Ioc a b = set.Iic b

theorem set.Iio_subset_Iic_union_Ioo {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_union_Ioo_eq_Iio {α : Type u} [linear_order α] {a b : α} :
a < bset.Iic a set.Ioo a b = set.Iio b

theorem set.Iic_subset_Iic_union_Icc {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_union_Icc_eq_Iic {α : Type u} [linear_order α] {a b : α} :
a bset.Iic a set.Icc a b = set.Iic b

theorem set.Iio_subset_Iic_union_Ico {α : Type u} [linear_order α] {a b : α} :

@[simp]
theorem set.Iic_union_Ico_eq_Iio {α : Type u} [linear_order α] {a b : α} :
a < bset.Iic a set.Ico a b = set.Iio b

Two finite intervals, I?o and Ic?

theorem set.Ioo_subset_Ioo_union_Ico {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioo_union_Ico_eq_Ioo {α : Type u} [linear_order α] {a b c : α} :
a < bb cset.Ioo a b set.Ico b c = set.Ioo a c

theorem set.Ico_subset_Ico_union_Ico {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ico_union_Ico_eq_Ico {α : Type u} [linear_order α] {a b c : α} :
a bb cset.Ico a b set.Ico b c = set.Ico a c

theorem set.Icc_subset_Ico_union_Icc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ico_union_Icc_eq_Icc {α : Type u} [linear_order α] {a b c : α} :
a bb cset.Ico a b set.Icc b c = set.Icc a c

theorem set.Ioc_subset_Ioo_union_Icc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioo_union_Icc_eq_Ioc {α : Type u} [linear_order α] {a b c : α} :
a < bb cset.Ioo a b set.Icc b c = set.Ioc a c

Two finite intervals, I?c and Io?

theorem set.Ioo_subset_Ioc_union_Ioo {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioc_union_Ioo_eq_Ioo {α : Type u} [linear_order α] {a b c : α} :
a bb < cset.Ioc a b set.Ioo b c = set.Ioo a c

theorem set.Ico_subset_Icc_union_Ioo {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Icc_union_Ioo_eq_Ico {α : Type u} [linear_order α] {a b c : α} :
a bb < cset.Icc a b set.Ioo b c = set.Ico a c

theorem set.Icc_subset_Icc_union_Ioc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Icc_union_Ioc_eq_Icc {α : Type u} [linear_order α] {a b c : α} :
a bb cset.Icc a b set.Ioc b c = set.Icc a c

theorem set.Ioc_subset_Ioc_union_Ioc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioc_union_Ioc_eq_Ioc {α : Type u} [linear_order α] {a b c : α} :
a bb cset.Ioc a b set.Ioc b c = set.Ioc a c

Two finite intervals with a common point

theorem set.Ioo_subset_Ioc_union_Ico {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioc_union_Ico_eq_Ioo {α : Type u} [linear_order α] {a b c : α} :
a < bb < cset.Ioc a b set.Ico b c = set.Ioo a c

theorem set.Ico_subset_Icc_union_Ico {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Icc_union_Ico_eq_Ico {α : Type u} [linear_order α] {a b c : α} :
a bb < cset.Icc a b set.Ico b c = set.Ico a c

theorem set.Icc_subset_Icc_union_Icc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Icc_union_Icc_eq_Icc {α : Type u} [linear_order α] {a b c : α} :
a bb cset.Icc a b set.Icc b c = set.Icc a c

theorem set.Ioc_subset_Ioc_union_Icc {α : Type u} [linear_order α] {a b c : α} :

@[simp]
theorem set.Ioc_union_Icc_eq_Ioc {α : Type u} [linear_order α] {a b c : α} :
a < bb cset.Ioc a b set.Icc b c = set.Ioc a c

@[simp]
theorem set.Iic_inter_Iic {α : Type u} [semilattice_inf α] {a b : α} :

@[simp]
theorem set.Iio_inter_Iio {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b : α} :

@[simp]
theorem set.Ici_inter_Ici {α : Type u} [semilattice_sup α] {a b : α} :

@[simp]
theorem set.Ioi_inter_Ioi {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b : α} :

theorem set.Icc_inter_Icc {α : Type u} [lattice α] {a₁ a₂ b₁ b₂ : α} :
set.Icc a₁ b₁ set.Icc a₂ b₂ = set.Icc (a₁ a₂) (b₁ b₂)

@[simp]
theorem set.Icc_inter_Icc_eq_singleton {α : Type u} [lattice α] {a b c : α} :
a bb cset.Icc a b set.Icc b c = {b}

theorem set.Ico_inter_Ico {α : Type u} [lattice α] [ht : is_total α has_le.le] {a₁ a₂ b₁ b₂ : α} :
set.Ico a₁ b₁ set.Ico a₂ b₂ = set.Ico (a₁ a₂) (b₁ b₂)

theorem set.Ioc_inter_Ioc {α : Type u} [lattice α] [ht : is_total α has_le.le] {a₁ a₂ b₁ b₂ : α} :
set.Ioc a₁ b₁ set.Ioc a₂ b₂ = set.Ioc (a₁ a₂) (b₁ b₂)

theorem set.Ioo_inter_Ioo {α : Type u} [lattice α] [ht : is_total α has_le.le] {a₁ a₂ b₁ b₂ : α} :
set.Ioo a₁ b₁ set.Ioo a₂ b₂ = set.Ioo (a₁ a₂) (b₁ b₂)

theorem set.Ioc_inter_Ioo_of_left_lt {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
b₁ < b₂set.Ioc a₁ b₁ set.Ioo a₂ b₂ = set.Ioc (max a₁ a₂) b₁

theorem set.Ioc_inter_Ioo_of_right_le {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
b₂ b₁set.Ioc a₁ b₁ set.Ioo a₂ b₂ = set.Ioo (max a₁ a₂) b₂

theorem set.Ioo_inter_Ioc_of_left_le {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
b₁ b₂set.Ioo a₁ b₁ set.Ioc a₂ b₂ = set.Ioo (max a₁ a₂) b₁

theorem set.Ioo_inter_Ioc_of_right_lt {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
b₂ < b₁set.Ioo a₁ b₁ set.Ioc a₂ b₂ = set.Ioc (max a₁ a₂) b₂

@[simp]
theorem set.Ico_diff_Iio {α : Type u} [decidable_linear_order α] {a b c : α} :
set.Ico a b \ set.Iio c = set.Ico (max a c) b

@[simp]
theorem set.Ico_inter_Iio {α : Type u} [decidable_linear_order α] {a b c : α} :
set.Ico a b set.Iio c = set.Ico a (min b c)

theorem set.Ioc_union_Ioc {α : Type u} [decidable_linear_order α] {a b c d : α} :
min a b max c dmin c d max a bset.Ioc a b set.Ioc c d = set.Ioc (min a c) (max b d)

@[simp]
theorem set.Ioc_union_Ioc_right {α : Type u} [decidable_linear_order α] {a b c : α} :
set.Ioc a b set.Ioc a c = set.Ioc a (max b c)

@[simp]
theorem set.Ioc_union_Ioc_left {α : Type u} [decidable_linear_order α] {a b c : α} :
set.Ioc a c set.Ioc b c = set.Ioc (min a b) c

@[simp]
theorem set.Ioc_union_Ioc_symm {α : Type u} [decidable_linear_order α] {a b : α} :
set.Ioc a b set.Ioc b a = set.Ioc (min a b) (max a b)

@[simp]
theorem set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u} [decidable_linear_order α] {a b c : α} :
set.Ioc a b set.Ioc b c set.Ioc c a = set.Ioc (min a (min b c)) (max a (max b c))

theorem set.nonempty_Ico_sdiff {α : Type u} [decidable_linear_ordered_add_comm_group α] {x dx y dy : α} :
dy < dx0 < dxnonempty (set.Ico x (x + dx) \ set.Ico y (y + dy))

If we remove a smaller interval from a larger, the result is nonempty