# mathlibdocumentation

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:

• `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 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_1} [preorder α] (a b : α) :
set α

Left-open right-open interval

Equations
• b = {x : α | a < x x < b}
Instances for `set.Ioo`
Instances for `↥set.Ioo`
def set.Ico {α : Type u_1} [preorder α] (a b : α) :
set α

Left-closed right-open interval

Equations
Instances for `set.Ico`
Instances for `↥set.Ico`
def set.Iio {α : Type u_1} [preorder α] (a : α) :
set α

Left-infinite right-open interval

Equations
• = {x : α | x < a}
Instances for `set.Iio`
Instances for `↥set.Iio`
def set.Icc {α : Type u_1} [preorder α] (a b : α) :
set α

Left-closed right-closed interval

Equations
Instances for `set.Icc`
Instances for `↥set.Icc`
def set.Iic {α : Type u_1} [preorder α] (b : α) :
set α

Left-infinite right-closed interval

Equations
• = {x : α | x b}
Instances for `set.Iic`
Instances for `↥set.Iic`
def set.Ioc {α : Type u_1} [preorder α] (a b : α) :
set α

Left-open right-closed interval

Equations
Instances for `set.Ioc`
Instances for `↥set.Ioc`
def set.Ici {α : Type u_1} [preorder α] (a : α) :
set α

Left-closed right-infinite interval

Equations
• = {x : α | a x}
Instances for `set.Ici`
Instances for `↥set.Ici`
def set.Ioi {α : Type u_1} [preorder α] (a : α) :
set α

Left-open right-infinite interval

Equations
• = {x : α | a < x}
Instances for `set.Ioi`
Instances for `↥set.Ioi`
theorem set.Ioo_def {α : Type u_1} [preorder α] (a b : α) :
{x : α | a < x x < b} = b
theorem set.Ico_def {α : Type u_1} [preorder α] (a b : α) :
{x : α | a x x < b} = b
theorem set.Iio_def {α : Type u_1} [preorder α] (a : α) :
{x : α | x < a} =
theorem set.Icc_def {α : Type u_1} [preorder α] (a b : α) :
{x : α | a x x b} = b
theorem set.Iic_def {α : Type u_1} [preorder α] (b : α) :
{x : α | x b} =
theorem set.Ioc_def {α : Type u_1} [preorder α] (a b : α) :
{x : α | a < x x b} = b
theorem set.Ici_def {α : Type u_1} [preorder α] (a : α) :
{x : α | a x} =
theorem set.Ioi_def {α : Type u_1} [preorder α] (a : α) :
{x : α | a < x} =
@[simp]
theorem set.mem_Ioo {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x < b
@[simp]
theorem set.mem_Ico {α : Type u_1} [preorder α] {a b x : α} :
x b a x x < b
@[simp]
theorem set.mem_Iio {α : Type u_1} [preorder α] {b x : α} :
x x < b
@[simp]
theorem set.mem_Icc {α : Type u_1} [preorder α] {a b x : α} :
x b a x x b
@[simp]
theorem set.mem_Iic {α : Type u_1} [preorder α] {b x : α} :
x x b
@[simp]
theorem set.mem_Ioc {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x b
@[simp]
theorem set.mem_Ici {α : Type u_1} [preorder α] {a x : α} :
x a x
@[simp]
theorem set.mem_Ioi {α : Type u_1} [preorder α] {a x : α} :
x a < x
@[protected, instance]
def set.decidable_mem_Ioo {α : Type u_1} [preorder α] {a b x : α} [decidable (a < x x < b)] :
Equations
@[protected, instance]
def set.decidable_mem_Ico {α : Type u_1} [preorder α] {a b x : α} [decidable (a x x < b)] :
Equations
@[protected, instance]
def set.decidable_mem_Iio {α : Type u_1} [preorder α] {b x : α} [decidable (x < b)] :
Equations
@[protected, instance]
def set.decidable_mem_Icc {α : Type u_1} [preorder α] {a b x : α} [decidable (a x x b)] :
Equations
@[protected, instance]
def set.decidable_mem_Iic {α : Type u_1} [preorder α] {b x : α} [decidable (x b)] :
Equations
@[protected, instance]
def set.decidable_mem_Ioc {α : Type u_1} [preorder α] {a b x : α} [decidable (a < x x b)] :
Equations
@[protected, instance]
def set.decidable_mem_Ici {α : Type u_1} [preorder α] {a x : α} [decidable (a x)] :
Equations
@[protected, instance]
def set.decidable_mem_Ioi {α : Type u_1} [preorder α] {a x : α} [decidable (a < x)] :
Equations
@[simp]
theorem set.left_mem_Ioo {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.left_mem_Ico {α : Type u_1} [preorder α] {a b : α} :
a b a < b
@[simp]
theorem set.left_mem_Icc {α : Type u_1} [preorder α] {a b : α} :
a b a b
@[simp]
theorem set.left_mem_Ioc {α : Type u_1} [preorder α] {a b : α} :
theorem set.left_mem_Ici {α : Type u_1} [preorder α] {a : α} :
a
@[simp]
theorem set.right_mem_Ioo {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.right_mem_Ico {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.right_mem_Icc {α : Type u_1} [preorder α] {a b : α} :
b b a b
@[simp]
theorem set.right_mem_Ioc {α : Type u_1} [preorder α] {a b : α} :
b b a < b
theorem set.right_mem_Iic {α : Type u_1} [preorder α] {a : α} :
a
@[simp]
theorem set.dual_Ici {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.dual_Iic {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.dual_Ioi {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.dual_Iio {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.dual_Icc {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.dual_Ioc {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.dual_Ico {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.dual_Ioo {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.nonempty_Icc {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem set.nonempty_Ico {α : Type u_1} [preorder α] {a b : α} :
(set.Ico a b).nonempty a < b
@[simp]
theorem set.nonempty_Ioc {α : Type u_1} [preorder α] {a b : α} :
(set.Ioc a b).nonempty a < b
@[simp]
theorem set.nonempty_Ici {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.nonempty_Iic {α : Type u_1} [preorder α] {a : α} :
@[simp]
theorem set.nonempty_Ioo {α : Type u_1} [preorder α] {a b : α}  :
(set.Ioo a b).nonempty a < b
@[simp]
theorem set.nonempty_Ioi {α : Type u_1} [preorder α] {a : α} [no_max_order α] :
@[simp]
theorem set.nonempty_Iio {α : Type u_1} [preorder α] {a : α} [no_min_order α] :
theorem set.nonempty_Icc_subtype {α : Type u_1} [preorder α] {a b : α} (h : a b) :
theorem set.nonempty_Ico_subtype {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
theorem set.nonempty_Ioc_subtype {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
@[protected, instance]
def set.nonempty_Ici_subtype {α : Type u_1} [preorder α] {a : α} :

An interval `Ici a` is nonempty.

@[protected, instance]
def set.nonempty_Iic_subtype {α : Type u_1} [preorder α] {a : α} :

An interval `Iic a` is nonempty.

theorem set.nonempty_Ioo_subtype {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
@[protected, instance]
def set.nonempty_Ioi_subtype {α : Type u_1} [preorder α] {a : α} [no_max_order α] :

In an order without maximal elements, the intervals `Ioi` are nonempty.

@[protected, instance]
def set.nonempty_Iio_subtype {α : Type u_1} [preorder α] {a : α} [no_min_order α] :

In an order without minimal elements, the intervals `Iio` are nonempty.

@[protected, instance]
def set.Iio.no_min_order {α : Type u_1} [preorder α] {a : α} [no_min_order α] :
@[protected, instance]
def set.Iic.no_min_order {α : Type u_1} [preorder α] {a : α} [no_min_order α] :
@[protected, instance]
def set.Ioi.no_max_order {α : Type u_1} [preorder α] {a : α} [no_max_order α] :
@[protected, instance]
def set.Ici.no_max_order {α : Type u_1} [preorder α] {a : α} [no_max_order α] :
@[simp]
theorem set.Icc_eq_empty {α : Type u_1} [preorder α] {a b : α} (h : ¬a b) :
b =
@[simp]
theorem set.Ico_eq_empty {α : Type u_1} [preorder α] {a b : α} (h : ¬a < b) :
b =
@[simp]
theorem set.Ioc_eq_empty {α : Type u_1} [preorder α] {a b : α} (h : ¬a < b) :
b =
@[simp]
theorem set.Ioo_eq_empty {α : Type u_1} [preorder α] {a b : α} (h : ¬a < b) :
b =
@[simp]
theorem set.Icc_eq_empty_of_lt {α : Type u_1} [preorder α] {a b : α} (h : b < a) :
b =
@[simp]
theorem set.Ico_eq_empty_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem set.Ioc_eq_empty_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem set.Ioo_eq_empty_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem set.Ico_self {α : Type u_1} [preorder α] (a : α) :
a =
@[simp]
theorem set.Ioc_self {α : Type u_1} [preorder α] (a : α) :
a =
@[simp]
theorem set.Ioo_self {α : Type u_1} [preorder α] (a : α) :
a =
theorem set.Ici_subset_Ici {α : Type u_1} [preorder α] {a b : α} :
b a
theorem set.Iic_subset_Iic {α : Type u_1} [preorder α] {a b : α} :
a b
theorem set.Ici_subset_Ioi {α : Type u_1} [preorder α] {a b : α} :
b < a
theorem set.Iic_subset_Iio {α : Type u_1} [preorder α] {a b : α} :
a < b
theorem set.Ioo_subset_Ioo {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
set.Ioo a₁ b₁ set.Ioo a₂ b₂
theorem set.Ioo_subset_Ioo_left {α : Type u_1} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
set.Ioo a₂ b set.Ioo a₁ b
theorem set.Ioo_subset_Ioo_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem set.Ico_subset_Ico {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
set.Ico a₁ b₁ set.Ico a₂ b₂
theorem set.Ico_subset_Ico_left {α : Type u_1} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
set.Ico a₂ b set.Ico a₁ b
theorem set.Ico_subset_Ico_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem set.Icc_subset_Icc {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
set.Icc a₁ b₁ set.Icc a₂ b₂
theorem set.Icc_subset_Icc_left {α : Type u_1} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
set.Icc a₂ b set.Icc a₁ b
theorem set.Icc_subset_Icc_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem set.Icc_subset_Ioo {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ < b₂) :
set.Icc a₁ b₁ set.Ioo a₂ b₂
theorem set.Icc_subset_Ici_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Icc_subset_Iic_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioc_subset_Iic_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioc_subset_Ioc {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ a₁) (h₂ : b₁ b₂) :
set.Ioc a₁ b₁ set.Ioc a₂ b₂
theorem set.Ioc_subset_Ioc_left {α : Type u_1} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
set.Ioc a₂ b set.Ioc a₁ b
theorem set.Ioc_subset_Ioc_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem set.Ico_subset_Ioo_left {α : Type u_1} [preorder α] {a₁ a₂ b : α} (h₁ : a₁ < a₂) :
set.Ico a₂ b set.Ioo a₁ b
theorem set.Ioc_subset_Ioo_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
b₁ b₂
theorem set.Icc_subset_Ico_right {α : Type u_1} [preorder α] {a b₁ b₂ : α} (h₁ : b₁ < b₂) :
b₁ b₂
theorem set.Ioo_subset_Ico_self {α : Type u_1} [preorder α] {a b : α} :
b b
theorem set.Ioo_subset_Ioc_self {α : Type u_1} [preorder α] {a b : α} :
b b
theorem set.Ico_subset_Icc_self {α : Type u_1} [preorder α] {a b : α} :
b b
theorem set.Ioc_subset_Icc_self {α : Type u_1} [preorder α] {a b : α} :
b b
theorem set.Ioo_subset_Icc_self {α : Type u_1} [preorder α] {a b : α} :
b b
theorem set.Ico_subset_Iio_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioo_subset_Iio_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioc_subset_Ioi_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioo_subset_Ioi_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioi_subset_Ici_self {α : Type u_1} [preorder α] {a : α} :
theorem set.Iio_subset_Iic_self {α : Type u_1} [preorder α] {a : α} :
theorem set.Ico_subset_Ici_self {α : Type u_1} [preorder α] {a b : α} :
b
theorem set.Ioi_ssubset_Ici_self {α : Type u_1} [preorder α] {a : α} :
theorem set.Iio_ssubset_Iic_self {α : Type u_1} [preorder α] {a : α} :
theorem set.Icc_subset_Icc_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Icc a₂ b₂ a₂ a₁ b₁ b₂
theorem set.Icc_subset_Ioo_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Ioo a₂ b₂ a₂ < a₁ b₁ < b₂
theorem set.Icc_subset_Ico_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Ico a₂ b₂ a₂ a₁ b₁ < b₂
theorem set.Icc_subset_Ioc_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Ioc a₂ b₂ a₂ < a₁ b₁ b₂
theorem set.Icc_subset_Iio_iff {α : Type u_1} [preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Iio b₂ b₁ < b₂
theorem set.Icc_subset_Ioi_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Ioi a₂ a₂ < a₁
theorem set.Icc_subset_Iic_iff {α : Type u_1} [preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.Iic b₂ b₁ b₂
theorem set.Icc_subset_Ici_iff {α : Type u_1} [preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ b₁) :
set.Icc a₁ b₁ set.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₂) :
set.Icc a₁ b₁ set.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₂) :
set.Icc a₁ b₁ set.Icc a₂ b₂
theorem set.Ioi_subset_Ioi {α : Type u_1} [preorder α] {a b : α} (h : a b) :

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_1} [preorder α] {a b : α} (h : a b) :

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

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_1} [preorder α] {a b : α} (h : a 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 : α} :
= b
theorem set.Ici_inter_Iio {α : Type u_1} [preorder α] {a b : α} :
= b
theorem set.Ioi_inter_Iic {α : Type u_1} [preorder α] {a b : α} :
= b
theorem set.Ioi_inter_Iio {α : Type u_1} [preorder α] {a b : α} :
= b
theorem set.Iic_inter_Ici {α : Type u_1} [preorder α] {a b : α} :
= a
theorem set.Iio_inter_Ici {α : Type u_1} [preorder α] {a b : α} :
= a
theorem set.Iic_inter_Ioi {α : Type u_1} [preorder α] {a b : α} :
= a
theorem set.Iio_inter_Ioi {α : Type u_1} [preorder α] {a b : α} :
= a
theorem set.mem_Icc_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x b) :
x b
theorem set.mem_Ico_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x b) :
x b
theorem set.mem_Ioc_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x b) :
x b
theorem set.mem_Icc_of_Ico {α : Type u_1} [preorder α] {a b x : α} (h : x b) :
x b
theorem set.mem_Icc_of_Ioc {α : Type u_1} [preorder α] {a b x : α} (h : x b) :
x b
theorem set.mem_Ici_of_Ioi {α : Type u_1} [preorder α] {a x : α} (h : x ) :
x
theorem set.mem_Iic_of_Iio {α : Type u_1} [preorder α] {a x : α} (h : x ) :
x
theorem set.Icc_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
b = ¬a b
theorem set.Ico_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
b = ¬a < b
theorem set.Ioc_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
b = ¬a < b
theorem set.Ioo_eq_empty_iff {α : Type u_1} [preorder α] {a b : α}  :
b = ¬a < b
theorem is_top.Iic_eq {α : Type u_1} [preorder α] {a : α} (h : is_top a) :
theorem is_bot.Ici_eq {α : Type u_1} [preorder α] {a : α} (h : is_bot a) :
theorem is_max.Ioi_eq {α : Type u_1} [preorder α] {a : α} (h : is_max a) :
theorem is_min.Iio_eq {α : Type u_1} [preorder α] {a : α} (h : is_min a) :
theorem set.Iic_inter_Ioc_of_le {α : Type u_1} [preorder α] {a b c : α} (h : a c) :
c = a
@[simp]
theorem set.Icc_self {α : Type u_1} (a : α) :
a = {a}
@[simp]
theorem set.Icc_eq_singleton_iff {α : Type u_1} {a b c : α} :
b = {c} a = c b = c
@[simp]
theorem set.Icc_diff_left {α : Type u_1} {a b : α} :
b \ {a} = b
@[simp]
theorem set.Icc_diff_right {α : Type u_1} {a b : α} :
b \ {b} = b
@[simp]
theorem set.Ico_diff_left {α : Type u_1} {a b : α} :
b \ {a} = b
@[simp]
theorem set.Ioc_diff_right {α : Type u_1} {a b : α} :
b \ {b} = b
@[simp]
theorem set.Icc_diff_both {α : Type u_1} {a b : α} :
b \ {a, b} = b
@[simp]
theorem set.Ici_diff_left {α : Type u_1} {a : α} :
\ {a} =
@[simp]
theorem set.Iic_diff_right {α : Type u_1} {a : α} :
\ {a} =
@[simp]
theorem set.Ico_diff_Ioo_same {α : Type u_1} {a b : α} (h : a < b) :
b \ b = {a}
@[simp]
theorem set.Ioc_diff_Ioo_same {α : Type u_1} {a b : α} (h : a < b) :
b \ b = {b}
@[simp]
theorem set.Icc_diff_Ico_same {α : Type u_1} {a b : α} (h : a b) :
b \ b = {b}
@[simp]
theorem set.Icc_diff_Ioc_same {α : Type u_1} {a b : α} (h : a b) :
b \ b = {a}
@[simp]
theorem set.Icc_diff_Ioo_same {α : Type u_1} {a b : α} (h : a b) :
b \ b = {a, b}
@[simp]
theorem set.Ici_diff_Ioi_same {α : Type u_1} {a : α} :
\ = {a}
@[simp]
theorem set.Iic_diff_Iio_same {α : Type u_1} {a : α} :
\ = {a}
@[simp]
theorem set.Ioi_union_left {α : Type u_1} {a : α} :
{a} =
@[simp]
theorem set.Iio_union_right {α : Type u_1} {a : α} :
{a} =
theorem set.Ioo_union_left {α : Type u_1} {a b : α} (hab : a < b) :
b {a} = b
theorem set.Ioo_union_right {α : Type u_1} {a b : α} (hab : a < b) :
b {b} = b
theorem set.Ioc_union_left {α : Type u_1} {a b : α} (hab : a b) :
b {a} = b
theorem set.Ico_union_right {α : Type u_1} {a b : α} (hab : a b) :
b {b} = b
@[simp]
theorem set.Ico_insert_right {α : Type u_1} {a b : α} (h : a b) :
(set.Ico a b) = b
@[simp]
theorem set.Ioc_insert_left {α : Type u_1} {a b : α} (h : a b) :
(set.Ioc a b) = b
@[simp]
theorem set.Ioo_insert_left {α : Type u_1} {a b : α} (h : a < b) :
(set.Ioo a b) = b
@[simp]
theorem set.Ioo_insert_right {α : Type u_1} {a b : α} (h : a < b) :
(set.Ioo a b) = b
@[simp]
theorem set.Iio_insert {α : Type u_1} {a : α} :
(set.Iio a) =
@[simp]
theorem set.Ioi_insert {α : Type u_1} {a : α} :
(set.Ioi a) =
theorem set.mem_Ici_Ioi_of_subset_of_subset {α : Type u_1} {a : α} {s : set α} (ho : s) (hc : s ) :
theorem set.mem_Iic_Iio_of_subset_of_subset {α : Type u_1} {a : α} {s : set α} (ho : s) (hc : s ) :
theorem set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u_1} {a b : α} {s : set α} (ho : b s) (hc : s b) :
s {set.Icc a b, b, b, b}
theorem set.eq_left_or_mem_Ioo_of_mem_Ico {α : Type u_1} {a b x : α} (hmem : x b) :
x = a x b
theorem set.eq_right_or_mem_Ioo_of_mem_Ioc {α : Type u_1} {a b x : α} (hmem : x b) :
x = b x b
theorem set.eq_endpoints_or_mem_Ioo_of_mem_Icc {α : Type u_1} {a b x : α} (hmem : x b) :
x = a x = b x b
theorem is_max.Ici_eq {α : Type u_1} {a : α} (h : is_max a) :
= {a}
theorem is_min.Iic_eq {α : Type u_1} {a : α} (h : is_min a) :
= {a}
@[simp]
theorem set.Ici_top {α : Type u_1} [order_top α] :
= {}
@[simp]
theorem set.Ioi_top {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem set.Iic_top {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem set.Icc_top {α : Type u_1} [preorder α] [order_top α] {a : α} :
=
@[simp]
theorem set.Ioc_top {α : Type u_1} [preorder α] [order_top α] {a : α} :
=
@[simp]
theorem set.Iic_bot {α : Type u_1} [order_bot α] :
= {}
@[simp]
theorem set.Iio_bot {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem set.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem set.Icc_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :
a =
@[simp]
theorem set.Ico_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :
a =
theorem set.Icc_bot_top {α : Type u_1}  :
theorem set.not_mem_Ici {α : Type u_1} [linear_order α] {a c : α} :
c c < a
theorem set.not_mem_Iic {α : Type u_1} [linear_order α] {b c : α} :
c b < c
theorem set.not_mem_Icc_of_lt {α : Type u_1} [linear_order α] {a b c : α} (ha : c < a) :
c b
theorem set.not_mem_Icc_of_gt {α : Type u_1} [linear_order α] {a b c : α} (hb : b < c) :
c b
theorem set.not_mem_Ico_of_lt {α : Type u_1} [linear_order α] {a b c : α} (ha : c < a) :
c b
theorem set.not_mem_Ioc_of_gt {α : Type u_1} [linear_order α] {a b c : α} (hb : b < c) :
c b
theorem set.not_mem_Ioi {α : Type u_1} [linear_order α] {a c : α} :
c c a
theorem set.not_mem_Iio {α : Type u_1} [linear_order α] {b c : α} :
c b c
theorem set.not_mem_Ioc_of_le {α : Type u_1} [linear_order α] {a b c : α} (ha : c a) :
c b
theorem set.not_mem_Ico_of_ge {α : Type u_1} [linear_order α] {a b c : α} (hb : b c) :
c b
theorem set.not_mem_Ioo_of_le {α : Type u_1} [linear_order α] {a b c : α} (ha : c a) :
c b
theorem set.not_mem_Ioo_of_ge {α : Type u_1} [linear_order α] {a b c : α} (hb : b c) :
c b
@[simp]
theorem set.compl_Iic {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.compl_Ici {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.compl_Iio {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.compl_Ioi {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.Ici_diff_Ici {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Ici_diff_Ioi {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Ioi_diff_Ioi {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Ioi_diff_Ici {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Iic_diff_Iic {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Iio_diff_Iic {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Iic_diff_Iio {α : Type u_1} [linear_order α] {a b : α} :
\ = b
@[simp]
theorem set.Iio_diff_Iio {α : Type u_1} [linear_order α] {a b : α} :
\ = b
theorem set.Ico_subset_Ico_iff {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) :
set.Ico a₁ b₁ set.Ico a₂ b₂ a₂ a₁ b₁ b₂
theorem set.Ioc_subset_Ioc_iff {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) :
set.Ioc a₁ b₁ set.Ioc a₂ b₂ b₁ b₂ a₂ a₁
theorem set.Ioo_subset_Ioo_iff {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) :
set.Ioo a₁ b₁ set.Ioo a₂ b₂ a₂ a₁ b₁ b₂
theorem set.Ico_eq_Ico_iff {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : 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_1} [linear_order α] {a b : α} :
a b
@[simp]
theorem set.Ioi_subset_Ici_iff {α : Type u_1} [linear_order α] {a b : α}  :
a b
@[simp]
theorem set.Iio_subset_Iio_iff {α : Type u_1} [linear_order α] {a b : α} :
a b
@[simp]
theorem set.Iio_subset_Iic_iff {α : Type u_1} [linear_order α] {a b : α}  :
a b

### Unions of adjacent intervals #

#### Two infinite intervals #

theorem set.Iic_union_Ioi_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.Iio_union_Ici_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.Iic_union_Ici_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
theorem set.Iio_union_Ioi_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
@[simp]
theorem set.Iic_union_Ici {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.Iio_union_Ici {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.Iic_union_Ioi {α : Type u_1} [linear_order α] {a : α} :
@[simp]
theorem set.Iio_union_Ioi {α : Type u_1} [linear_order α] {a : α} :
= {a}

#### A finite and an infinite interval #

theorem set.Ioo_union_Ioi' {α : Type u_1} [linear_order α] {a b c : α} (h₁ : c < b) :
b = set.Ioi c)
theorem set.Ioo_union_Ioi {α : Type u_1} [linear_order α] {a b c : α} (h : c < ) :
b = set.Ioi c)
theorem set.Ioi_subset_Ioo_union_Ici {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Ioo_union_Ici_eq_Ioi {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
b =
theorem set.Ici_subset_Ico_union_Ici {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Ico_union_Ici_eq_Ici {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Ico_union_Ici' {α : Type u_1} [linear_order α] {a b c : α} (h₁ : c b) :
b = set.Ici c)
theorem set.Ico_union_Ici {α : Type u_1} [linear_order α] {a b c : α} (h : c ) :
b = set.Ici c)
theorem set.Ioi_subset_Ioc_union_Ioi {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Ioc_union_Ioi_eq_Ioi {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Ioc_union_Ioi' {α : Type u_1} [linear_order α] {a b c : α} (h₁ : c b) :
b = set.Ioi c)
theorem set.Ioc_union_Ioi {α : Type u_1} [linear_order α] {a b c : α} (h : c ) :
b = set.Ioi c)
theorem set.Ici_subset_Icc_union_Ioi {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Icc_union_Ioi_eq_Ici {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Ioi_subset_Ioc_union_Ici {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Ioc_union_Ici_eq_Ioi {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
b =
theorem set.Ici_subset_Icc_union_Ici {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Icc_union_Ici_eq_Ici {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Icc_union_Ici' {α : Type u_1} [linear_order α] {a b c : α} (h₁ : c b) :
b = set.Ici c)
theorem set.Icc_union_Ici {α : Type u_1} [linear_order α] {a b c : α} (h : c ) :
b = set.Ici c)

#### An infinite and a finite interval #

theorem set.Iic_subset_Iio_union_Icc {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iio_union_Icc_eq_Iic {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Iio_subset_Iio_union_Ico {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iio_union_Ico_eq_Iio {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Iio_union_Ico' {α : Type u_1} [linear_order α] {b c d : α} (h₁ : c b) :
d = set.Iio d)
theorem set.Iio_union_Ico {α : Type u_1} [linear_order α] {b c d : α} (h : b) :
d = set.Iio d)
theorem set.Iic_subset_Iic_union_Ioc {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iic_union_Ioc_eq_Iic {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Iic_union_Ioc' {α : Type u_1} [linear_order α] {b c d : α} (h₁ : c < b) :
d = set.Iic d)
theorem set.Iic_union_Ioc {α : Type u_1} [linear_order α] {b c d : α} (h : < b) :
d = set.Iic d)
theorem set.Iio_subset_Iic_union_Ioo {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iic_union_Ioo_eq_Iio {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
b =
theorem set.Iio_union_Ioo' {α : Type u_1} [linear_order α] {b c d : α} (h₁ : c < b) :
d = set.Iio d)
theorem set.Iio_union_Ioo {α : Type u_1} [linear_order α] {b c d : α} (h : < b) :
d = set.Iio d)
theorem set.Iic_subset_Iic_union_Icc {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iic_union_Icc_eq_Iic {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b =
theorem set.Iic_union_Icc' {α : Type u_1} [linear_order α] {b c d : α} (h₁ : c b) :
d = set.Iic d)
theorem set.Iic_union_Icc {α : Type u_1} [linear_order α] {b c d : α} (h : b) :
d = set.Iic d)
theorem set.Iio_subset_Iic_union_Ico {α : Type u_1} [linear_order α] {a b : α} :
b
@[simp]
theorem set.Iic_union_Ico_eq_Iio {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
b =

#### Two finite intervals, `I?o` and `Ic?`#

theorem set.Ioo_subset_Ioo_union_Ico {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioo_union_Ico_eq_Ioo {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : b c) :
b c = c
theorem set.Ico_subset_Ico_union_Ico {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ico_union_Ico_eq_Ico {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem set.Ico_union_Ico' {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : c b) (h₂ : a d) :
b d = set.Ico c) d)
theorem set.Ico_union_Ico {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : ) (h₂ : ) :
b d = set.Ico c) d)
theorem set.Icc_subset_Ico_union_Icc {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ico_union_Icc_eq_Icc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem set.Ioc_subset_Ioo_union_Icc {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioo_union_Icc_eq_Ioc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : b c) :
b c = c

#### Two finite intervals, `I?c` and `Io?`#

theorem set.Ioo_subset_Ioc_union_Ioo {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioc_union_Ioo_eq_Ioo {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b < c) :
b c = c
theorem set.Ico_subset_Icc_union_Ioo {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Icc_union_Ioo_eq_Ico {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b < c) :
b c = c
theorem set.Icc_subset_Icc_union_Ioc {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Icc_union_Ioc_eq_Icc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem set.Ioc_subset_Ioc_union_Ioc {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioc_union_Ioc_eq_Ioc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem set.Ioc_union_Ioc' {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : c b) (h₂ : a d) :
b d = set.Ioc c) d)
theorem set.Ioc_union_Ioc {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : ) (h₂ : ) :
b d = set.Ioc c) d)

#### Two finite intervals with a common point #

theorem set.Ioo_subset_Ioc_union_Ico {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioc_union_Ico_eq_Ioo {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : b < c) :
b c = c
theorem set.Ico_subset_Icc_union_Ico {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Icc_union_Ico_eq_Ico {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b < c) :
b c = c
theorem set.Icc_subset_Icc_union_Icc {α : Type u_1} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Icc_union_Icc_eq_Icc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem set.Icc_union_Icc' {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : c b) (h₂ : a d) :
b d = set.Icc c) d)
theorem set.Icc_union_Icc {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : < ) (h₂ : < ) :
b d = set.Icc c) 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} [linear_order α] {a b c : α} :
c b c
@[simp]
theorem set.Ioc_union_Icc_eq_Ioc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : b c) :
b c = c
theorem set.Ioo_union_Ioo' {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : c < b) (h₂ : a < d) :
b d = set.Ioo c) d)
theorem set.Ioo_union_Ioo {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : < ) (h₂ : < ) :
b d = set.Ioo c) d)
@[simp]
theorem set.Iic_inter_Iic {α : Type u_1} {a b : α} :
= set.Iic (a b)
@[simp]
theorem set.Ioc_inter_Iic {α : Type u_1} (a b c : α) :
b = (b c)
@[simp]
theorem set.Ici_inter_Ici {α : Type u_1} {a b : α} :
= set.Ici (a b)
@[simp]
theorem set.Ico_inter_Ici {α : Type u_1} (a b c : α) :
b = set.Ico (a c) b
theorem set.Icc_inter_Icc {α : Type u_1} [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_1} [lattice α] {a b c : α} (hab : a b) (hbc : b c) :
b c = {b}
@[simp]
theorem set.Ioi_inter_Ioi {α : Type u_1} [linear_order α] {a b : α} :
= set.Ioi (a b)
@[simp]
theorem set.Iio_inter_Iio {α : Type u_1} [linear_order α] {a b : α} :
= set.Iio (a b)
theorem set.Ico_inter_Ico {α : Type u_1} [linear_order α] {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_1} [linear_order α] {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_1} [linear_order α] {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_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₁ < b₂) :
set.Ioc a₁ b₁ set.Ioo a₂ b₂ = set.Ioc a₂) b₁
theorem set.Ioc_inter_Ioo_of_right_le {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₂ b₁) :
set.Ioc a₁ b₁ set.Ioo a₂ b₂ = set.Ioo a₂) b₂
theorem set.Ioo_inter_Ioc_of_left_le {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₁ b₂) :
set.Ioo a₁ b₁ set.Ioc a₂ b₂ = set.Ioo a₂) b₁
theorem set.Ioo_inter_Ioc_of_right_lt {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₂ < b₁) :
set.Ioo a₁ b₁ set.Ioc a₂ b₂ = set.Ioc a₂) b₂
@[simp]
theorem set.Ico_diff_Iio {α : Type u_1} [linear_order α] {a b c : α} :
b \ = set.Ico c) b
@[simp]
theorem set.Ioc_diff_Ioi {α : Type u_1} [linear_order α] {a b c : α} :
b \ = c)
@[simp]
theorem set.Ioc_inter_Ioi {α : Type u_1} [linear_order α] {a b c : α} :
b = set.Ioc (a c) b
@[simp]
theorem set.Ico_inter_Iio {α : Type u_1} [linear_order α] {a b c : α} :
b = c)
@[simp]
theorem set.Ioc_diff_Iic {α : Type u_1} [linear_order α] {a b c : α} :
b \ = set.Ioc c) b
@[simp]
theorem set.Ioc_union_Ioc_right {α : Type u_1} [linear_order α] {a b c : α} :
b c = c)
@[simp]
theorem set.Ioc_union_Ioc_left {α : Type u_1} [linear_order α] {a b c : α} :
c c = set.Ioc b) c
@[simp]
theorem set.Ioc_union_Ioc_symm {α : Type u_1} [linear_order α] {a b : α} :
b a = set.Ioc b) b)
@[simp]
theorem set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u_1} [linear_order α] {a b c : α} :
b c a = set.Ioc c)) c))

### Closed intervals in `α × β`#

@[simp]
theorem set.Iic_prod_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
×ˢ = set.Iic (a, b)
@[simp]
theorem set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
×ˢ = set.Ici (a, b)
theorem set.Ici_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α × β) :
theorem set.Iic_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α × β) :
@[simp]
theorem set.Icc_prod_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) (b₁ b₂ : β) :
set.Icc a₁ a₂ ×ˢ set.Icc b₁ b₂ = set.Icc (a₁, b₁) (a₂, b₂)
theorem set.Icc_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a b : α × β) :
b = b.fst ×ˢ b.snd

### Lemmas about membership of arithmetic operations #

`inv_mem_Ixx_iff`, `sub_mem_Ixx_iff`

theorem set.neg_mem_Icc_iff {α : Type u_1} {a c d : α} :
-a d a set.Icc (-d) (-c)
theorem set.inv_mem_Icc_iff {α : Type u_1} {a c d : α} :
theorem set.neg_mem_Ico_iff {α : Type u_1} {a c d : α} :
-a d a set.Ioc (-d) (-c)
theorem set.inv_mem_Ico_iff {α : Type u_1} {a c d : α} :
theorem set.inv_mem_Ioc_iff {α : Type u_1} {a c d : α} :
theorem set.neg_mem_Ioc_iff {α : Type u_1} {a c d : α} :
-a d a set.Ico (-d) (-c)
theorem set.inv_mem_Ioo_iff {α : Type u_1} {a c d : α} :
theorem set.neg_mem_Ioo_iff {α : Type u_1} {a c d : α} :
-a d a set.Ioo (-d) (-c)

`add_mem_Ixx_iff_left`

theorem set.add_mem_Icc_iff_left {α : Type u_1} {a b c d : α} :
a + b d a set.Icc (c - b) (d - b)
theorem set.add_mem_Ico_iff_left {α : Type u_1} {a b c d : α} :
a + b d a set.Ico (c - b) (d - b)
theorem set.add_mem_Ioc_iff_left {α : Type u_1} {a b c d : α} :
a + b d a set.Ioc (c - b) (d - b)
theorem set.add_mem_Ioo_iff_left {α : Type u_1} {a b c d : α} :
a + b d a set.Ioo (c - b) (d - b)

`add_mem_Ixx_iff_right`

theorem set.add_mem_Icc_iff_right {α : Type u_1} {a b c d : α} :
a + b d b set.Icc (c - a) (d - a)
theorem set.add_mem_Ico_iff_right {α : Type u_1} {a b c d : α} :
a + b d b set.Ico (c - a) (d - a)
theorem set.add_mem_Ioc_iff_right {α : Type u_1} {a b c d : α} :
a + b d b set.Ioc (c - a) (d - a)
theorem set.add_mem_Ioo_iff_right {α : Type u_1} {a b c d : α} :
a + b d b set.Ioo (c - a) (d - a)

`sub_mem_Ixx_iff_left`

theorem set.sub_mem_Icc_iff_left {α : Type u_1} {a b c d : α} :
a - b d a set.Icc (c + b) (d + b)
theorem set.sub_mem_Ico_iff_left {α : Type u_1} {a b c d : α} :
a - b d a set.Ico (c + b) (d + b)
theorem set.sub_mem_Ioc_iff_left {α : Type u_1} {a b c d : α} :
a - b d a set.Ioc (c + b) (d + b)
theorem set.sub_mem_Ioo_iff_left {α : Type u_1} {a b c d : α} :
a - b d a set.Ioo (c + b) (d + b)

`sub_mem_Ixx_iff_right`

theorem set.sub_mem_Icc_iff_right {α : Type u_1} {a b c d : α} :
a - b d b set.Icc (a - d) (a - c)
theorem set.sub_mem_Ico_iff_right {α : Type u_1} {a b c d : α} :
a - b d b set.Ioc (a - d) (a - c)
theorem set.sub_mem_Ioc_iff_right {α : Type u_1} {a b c d : α} :
a - b d b set.Ico (a - d) (a - c)
theorem set.sub_mem_Ioo_iff_right {α : Type u_1} {a b c d : α} :
a - b d b set.Ioo (a - d) (a - c)
theorem set.mem_Icc_iff_abs_le {R : Type u_1} {x y z : R} :
|x - y| z y set.Icc (x - z) (x + z)
theorem set.nonempty_Ico_sdiff {α : Type u_1} {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) :
nonempty (set.Ico x (x + dx) \ (y + dy))

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

@[simp]
theorem order_iso.preimage_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (b : β) :
@[simp]
theorem order_iso.preimage_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' b = set.Icc ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' b = set.Ico ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' b = set.Ioc ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.preimage_Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : β) :
e ⁻¹' b = set.Ioo ((e.symm) a) ((e.symm) b)
@[simp]
theorem order_iso.image_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
@[simp]
theorem order_iso.image_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
@[simp]
theorem order_iso.image_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
@[simp]
theorem order_iso.image_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
@[simp]
theorem order_iso.image_Ioo {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : α) :
e '' b = set.Ioo (e a) (e b)
@[simp]
theorem order_iso.image_Ioc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : α) :
e '' b = set.Ioc (e a) (e b)
@[simp]
theorem order_iso.image_Ico {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : α) :
e '' b = set.Ico (e a) (e b)
@[simp]
theorem order_iso.image_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a b : α) :
e '' b = set.Icc (e a) (e b)
def order_iso.Iic_top {α : Type u_1} [preorder α] [order_top α] :

Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element

Equations
def order_iso.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :

Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element

Equations

### Lemmas about intervals in dense orders #

@[protected, instance]
def set.Ioo.no_min_order (α : Type u_1) [preorder α] {x y : α} :
@[protected, instance]
def set.Ioc.no_min_order (α : Type u_1) [preorder α] {x y : α} :
@[protected, instance]
def set.Ioi.no_min_order (α : Type u_1) [preorder α] {x : α} :
@[protected, instance]
def set.Ioo.no_max_order (α : Type u_1) [preorder α] {x y : α} :
@[protected, instance]
def set.Ico.no_max_order (α : Type u_1) [preorder α] {x y : α} :
@[protected, instance]
def set.Iio.no_max_order (α : Type u_1) [preorder α] {x : α} :