mathlib3 documentation

data.set.intervals.basic

Intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
def set.Ioo {α : Type u_1} [preorder α] (a b : α) :
set α

Left-open right-open interval

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

Left-closed right-open interval

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

Left-infinite right-open interval

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

Left-closed right-closed interval

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

Left-infinite right-closed interval

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

Left-open right-closed interval

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

Left-closed right-infinite interval

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

Left-open right-infinite interval

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

An interval Ici a is nonempty.

source
@[protected, instance]
def set.nonempty_Iic_subtype {α : Type u_1} [preorder α] {a : α} :
nonempty ↥(set.Iic a)

An interval Iic a is nonempty.

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

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

source
@[protected, instance]
def set.nonempty_Iio_subtype {α : Type u_1} [preorder α] {a : α} [no_min_order α] :
nonempty ↥(set.Iio a)

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

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

source
theorem set.Ioi_subset_Ici {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :
set.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.

source
theorem set.Iio_subset_Iio {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :
set.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.

source
theorem set.Iio_subset_Iic {α : Type u_1} [preorder α] {a b : α} (h : a ≤ b) :
set.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.

source
theorem set.Ici_inter_Iic {α : Type u_1} [preorder α] {a b : α} :
set.Ici a ∩ set.Iic b = set.Icc a b
source
theorem set.Ici_inter_Iio {α : Type u_1} [preorder α] {a b : α} :
set.Ici a ∩ set.Iio b = set.Ico a b
source
theorem set.Ioi_inter_Iic {α : Type u_1} [preorder α] {a b : α} :
set.Ioi a ∩ set.Iic b = set.Ioc a b
source
theorem set.Ioi_inter_Iio {α : Type u_1} [preorder α] {a b : α} :
set.Ioi a ∩ set.Iio b = set.Ioo a b
source
theorem set.Iic_inter_Ici {α : Type u_1} [preorder α] {a b : α} :
set.Iic a ∩ set.Ici b = set.Icc b a
source
theorem set.Iio_inter_Ici {α : Type u_1} [preorder α] {a b : α} :
set.Iio a ∩ set.Ici b = set.Ico b a
source
theorem set.Iic_inter_Ioi {α : Type u_1} [preorder α] {a b : α} :
set.Iic a ∩ set.Ioi b = set.Ioc b a
source
theorem set.Iio_inter_Ioi {α : Type u_1} [preorder α] {a b : α} :
set.Iio a ∩ set.Ioi b = set.Ioo b a
source
theorem set.mem_Icc_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Icc a b
source
theorem set.mem_Ico_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Ico a b
source
theorem set.mem_Ioc_of_Ioo {α : Type u_1} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Ioc a b
source
theorem set.mem_Icc_of_Ico {α : Type u_1} [preorder α] {a b x : α} (h : x ∈ set.Ico a b) :
x ∈ set.Icc a b
source
theorem set.mem_Icc_of_Ioc {α : Type u_1} [preorder α] {a b x : α} (h : x ∈ set.Ioc a b) :
x ∈ set.Icc a b
source
theorem set.mem_Ici_of_Ioi {α : Type u_1} [preorder α] {a x : α} (h : x ∈ set.Ioi a) :
x ∈ set.Ici a
source
theorem set.mem_Iic_of_Iio {α : Type u_1} [preorder α] {a x : α} (h : x ∈ set.Iio a) :
x ∈ set.Iic a
source
theorem set.Icc_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
set.Icc a b = ∅ ↔ ¬a ≤ b
source
theorem set.Ico_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
set.Ico a b = ∅ ↔ ¬a < b
source
theorem set.Ioc_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} :
set.Ioc a b = ∅ ↔ ¬a < b
source
theorem set.Ioo_eq_empty_iff {α : Type u_1} [preorder α] {a b : α} [densely_ordered α] :
set.Ioo a b = ∅ ↔ ¬a < b
source
theorem is_top.Iic_eq {α : Type u_1} [preorder α] {a : α} (h : is_top a) :
set.Iic a = set.univ
source
theorem is_bot.Ici_eq {α : Type u_1} [preorder α] {a : α} (h : is_bot a) :
set.Ici a = set.univ
source
theorem is_max.Ioi_eq {α : Type u_1} [preorder α] {a : α} (h : is_max a) :
set.Ioi a = ∅
source
theorem is_min.Iio_eq {α : Type u_1} [preorder α] {a : α} (h : is_min a) :
set.Iio a = ∅
source
theorem set.Iic_inter_Ioc_of_le {α : Type u_1} [preorder α] {a b c : α} (h : a ≤ c) :
set.Iic a ∩ set.Ioc b c = set.Ioc b a
source
theorem set.not_mem_Icc_of_lt {α : Type u_1} [preorder α] {a b c : α} (ha : c < a) :
c ∉ set.Icc a b
source
theorem set.not_mem_Icc_of_gt {α : Type u_1} [preorder α] {a b c : α} (hb : b < c) :
c ∉ set.Icc a b
source
theorem set.not_mem_Ico_of_lt {α : Type u_1} [preorder α] {a b c : α} (ha : c < a) :
c ∉ set.Ico a b
source
theorem set.not_mem_Ioc_of_gt {α : Type u_1} [preorder α] {a b c : α} (hb : b < c) :
c ∉ set.Ioc a b
source
@[simp]
theorem set.not_mem_Ioi_self {α : Type u_1} [preorder α] {a : α} :
a ∉ set.Ioi a
source
@[simp]
theorem set.not_mem_Iio_self {α : Type u_1} [preorder α] {b : α} :
b ∉ set.Iio b
source
theorem set.not_mem_Ioc_of_le {α : Type u_1} [preorder α] {a b c : α} (ha : c ≤ a) :
c ∉ set.Ioc a b
source
theorem set.not_mem_Ico_of_ge {α : Type u_1} [preorder α] {a b c : α} (hb : b ≤ c) :
c ∉ set.Ico a b
source
theorem set.not_mem_Ioo_of_le {α : Type u_1} [preorder α] {a b c : α} (ha : c ≤ a) :
c ∉ set.Ioo a b
source
theorem set.not_mem_Ioo_of_ge {α : Type u_1} [preorder α] {a b c : α} (hb : b ≤ c) :
c ∉ set.Ioo a b
source
@[simp]
theorem set.Icc_self {α : Type u_1} [partial_order α] (a : α) :
set.Icc a a = {a}
source
@[simp]
theorem set.Icc_eq_singleton_iff {α : Type u_1} [partial_order α] {a b c : α} :
set.Icc a b = {c} ↔ a = c ∧ b = c
source
@[simp]
theorem set.Icc_diff_left {α : Type u_1} [partial_order α] {a b : α} :
set.Icc a b \ {a} = set.Ioc a b
source
@[simp]
theorem set.Icc_diff_right {α : Type u_1} [partial_order α] {a b : α} :
set.Icc a b \ {b} = set.Ico a b
source
@[simp]
theorem set.Ico_diff_left {α : Type u_1} [partial_order α] {a b : α} :
set.Ico a b \ {a} = set.Ioo a b
source
@[simp]
theorem set.Ioc_diff_right {α : Type u_1} [partial_order α] {a b : α} :
set.Ioc a b \ {b} = set.Ioo a b
source
@[simp]
theorem set.Icc_diff_both {α : Type u_1} [partial_order α] {a b : α} :
set.Icc a b \ {a, b} = set.Ioo a b
source
@[simp]
theorem set.Ici_diff_left {α : Type u_1} [partial_order α] {a : α} :
set.Ici a \ {a} = set.Ioi a
source
@[simp]
theorem set.Iic_diff_right {α : Type u_1} [partial_order α] {a : α} :
set.Iic a \ {a} = set.Iio a
source
@[simp]
theorem set.Ico_diff_Ioo_same {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :
set.Ico a b \ set.Ioo a b = {a}
source
@[simp]
theorem set.Ioc_diff_Ioo_same {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :
set.Ioc a b \ set.Ioo a b = {b}
source
@[simp]
theorem set.Icc_diff_Ico_same {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :
set.Icc a b \ set.Ico a b = {b}
source
@[simp]
theorem set.Icc_diff_Ioc_same {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :
set.Icc a b \ set.Ioc a b = {a}
source
@[simp]
theorem set.Icc_diff_Ioo_same {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :
set.Icc a b \ set.Ioo a b = {a, b}
source
@[simp]
theorem set.Ici_diff_Ioi_same {α : Type u_1} [partial_order α] {a : α} :
set.Ici a \ set.Ioi a = {a}
source
@[simp]
theorem set.Iic_diff_Iio_same {α : Type u_1} [partial_order α] {a : α} :
set.Iic a \ set.Iio a = {a}
source
@[simp]
theorem set.Ioi_union_left {α : Type u_1} [partial_order α] {a : α} :
set.Ioi a ∪ {a} = set.Ici a
source
@[simp]
theorem set.Iio_union_right {α : Type u_1} [partial_order α] {a : α} :
set.Iio a ∪ {a} = set.Iic a
source
theorem set.Ioo_union_left {α : Type u_1} [partial_order α] {a b : α} (hab : a < b) :
set.Ioo a b ∪ {a} = set.Ico a b
source
theorem set.Ioo_union_right {α : Type u_1} [partial_order α] {a b : α} (hab : a < b) :
set.Ioo a b ∪ {b} = set.Ioc a b
source
theorem set.Ioc_union_left {α : Type u_1} [partial_order α] {a b : α} (hab : a ≤ b) :
set.Ioc a b ∪ {a} = set.Icc a b
source
theorem set.Ico_union_right {α : Type u_1} [partial_order α] {a b : α} (hab : a ≤ b) :
set.Ico a b ∪ {b} = set.Icc a b
source
@[simp]
theorem set.Ico_insert_right {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :
has_insert.insert b (set.Ico a b) = set.Icc a b
source
@[simp]
theorem set.Ioc_insert_left {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :
has_insert.insert a (set.Ioc a b) = set.Icc a b
source
@[simp]
theorem set.Ioo_insert_left {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :
has_insert.insert a (set.Ioo a b) = set.Ico a b
source
@[simp]
theorem set.Ioo_insert_right {α : Type u_1} [partial_order α] {a b : α} (h : a < b) :
has_insert.insert b (set.Ioo a b) = set.Ioc a b
source
@[simp]
theorem set.Iio_insert {α : Type u_1} [partial_order α] {a : α} :
has_insert.insert a (set.Iio a) = set.Iic a
source
@[simp]
theorem set.Ioi_insert {α : Type u_1} [partial_order α] {a : α} :
has_insert.insert a (set.Ioi a) = set.Ici a
source
theorem set.mem_Ici_Ioi_of_subset_of_subset {α : Type u_1} [partial_order α] {a : α} {s : set α} (ho : set.Ioi a ⊆ s) (hc : s ⊆ set.Ici a) :
s ∈ {set.Ici a, set.Ioi a}
source
theorem set.mem_Iic_Iio_of_subset_of_subset {α : Type u_1} [partial_order α] {a : α} {s : set α} (ho : set.Iio a ⊆ s) (hc : s ⊆ set.Iic a) :
s ∈ {set.Iic a, set.Iio a}
source
theorem set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u_1} [partial_order α] {a b : α} {s : set α} (ho : set.Ioo a b ⊆ s) (hc : s ⊆ set.Icc a b) :
s ∈ {set.Icc a b, set.Ico a b, set.Ioc a b, set.Ioo a b}
source
theorem set.eq_left_or_mem_Ioo_of_mem_Ico {α : Type u_1} [partial_order α] {a b x : α} (hmem : x ∈ set.Ico a b) :
x = a ∨ x ∈ set.Ioo a b
source
theorem set.eq_right_or_mem_Ioo_of_mem_Ioc {α : Type u_1} [partial_order α] {a b x : α} (hmem : x ∈ set.Ioc a b) :
x = b ∨ x ∈ set.Ioo a b
source
theorem set.eq_endpoints_or_mem_Ioo_of_mem_Icc {α : Type u_1} [partial_order α] {a b x : α} (hmem : x ∈ set.Icc a b) :
x = a ∨ x = b ∨ x ∈ set.Ioo a b
source
theorem is_max.Ici_eq {α : Type u_1} [partial_order α] {a : α} (h : is_max a) :
set.Ici a = {a}
source
theorem is_min.Iic_eq {α : Type u_1} [partial_order α] {a : α} (h : is_min a) :
set.Iic a = {a}
source
theorem set.Ici_injective {α : Type u_1} [partial_order α] :
function.injective set.Ici
source
theorem set.Iic_injective {α : Type u_1} [partial_order α] :
function.injective set.Iic
source
theorem set.Ici_inj {α : Type u_1} [partial_order α] {a b : α} :
set.Ici a = set.Ici b ↔ a = b
source
theorem set.Iic_inj {α : Type u_1} [partial_order α] {a b : α} :
set.Iic a = set.Iic b ↔ a = b
source
@[simp]
theorem set.Ici_top {α : Type u_1} [partial_order α] [order_top α] :
set.Ici ⊤ = {⊤}
source
@[simp]
theorem set.Ioi_top {α : Type u_1} [preorder α] [order_top α] :
set.Ioi ⊤ = ∅
source
@[simp]
theorem set.Iic_top {α : Type u_1} [preorder α] [order_top α] :
set.Iic ⊤ = set.univ
source
@[simp]
theorem set.Icc_top {α : Type u_1} [preorder α] [order_top α] {a : α} :
set.Icc a ⊤ = set.Ici a
source
@[simp]
theorem set.Ioc_top {α : Type u_1} [preorder α] [order_top α] {a : α} :
set.Ioc a ⊤ = set.Ioi a
source
@[simp]
theorem set.Iic_bot {α : Type u_1} [partial_order α] [order_bot α] :
set.Iic ⊥ = {⊥}
source
@[simp]
theorem set.Iio_bot {α : Type u_1} [preorder α] [order_bot α] :
set.Iio ⊥ = ∅
source
@[simp]
theorem set.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
set.Ici ⊥ = set.univ
source
@[simp]
theorem set.Icc_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :
set.Icc ⊥ a = set.Iic a
source
@[simp]
theorem set.Ico_bot {α : Type u_1} [preorder α] [order_bot α] {a : α} :
set.Ico ⊥ a = set.Iio a
source
theorem set.Icc_bot_top {α : Type u_1} [partial_order α] [bounded_order α] :
set.Icc ⊥ ⊤ = set.univ
source
theorem set.not_mem_Ici {α : Type u_1} [linear_order α] {a c : α} :
c ∉ set.Ici a ↔ c < a
source
theorem set.not_mem_Iic {α : Type u_1} [linear_order α] {b c : α} :
c ∉ set.Iic b ↔ b < c
source
theorem set.not_mem_Ioi {α : Type u_1} [linear_order α] {a c : α} :
c ∉ set.Ioi a ↔ c ≤ a
source
theorem set.not_mem_Iio {α : Type u_1} [linear_order α] {b c : α} :
c ∉ set.Iio b ↔ b ≤ c
source
@[simp]
theorem set.compl_Iic {α : Type u_1} [linear_order α] {a : α} :
(set.Iic a)ᶜ = set.Ioi a
source
@[simp]
theorem set.compl_Ici {α : Type u_1} [linear_order α] {a : α} :
(set.Ici a)ᶜ = set.Iio a
source
@[simp]
theorem set.compl_Iio {α : Type u_1} [linear_order α] {a : α} :
(set.Iio a)ᶜ = set.Ici a
source
@[simp]
theorem set.compl_Ioi {α : Type u_1} [linear_order α] {a : α} :
(set.Ioi a)ᶜ = set.Iic a
source
@[simp]
theorem set.Ici_diff_Ici {α : Type u_1} [linear_order α] {a b : α} :
set.Ici a \ set.Ici b = set.Ico a b
source
@[simp]
theorem set.Ici_diff_Ioi {α : Type u_1} [linear_order α] {a b : α} :
set.Ici a \ set.Ioi b = set.Icc a b
source
@[simp]
theorem set.Ioi_diff_Ioi {α : Type u_1} [linear_order α] {a b : α} :
set.Ioi a \ set.Ioi b = set.Ioc a b
source
@[simp]
theorem set.Ioi_diff_Ici {α : Type u_1} [linear_order α] {a b : α} :
set.Ioi a \ set.Ici b = set.Ioo a b
source
@[simp]
theorem set.Iic_diff_Iic {α : Type u_1} [linear_order α] {a b : α} :
set.Iic b \ set.Iic a = set.Ioc a b
source
@[simp]
theorem set.Iio_diff_Iic {α : Type u_1} [linear_order α] {a b : α} :
set.Iio b \ set.Iic a = set.Ioo a b
source
@[simp]
theorem set.Iic_diff_Iio {α : Type u_1} [linear_order α] {a b : α} :
set.Iic b \ set.Iio a = set.Icc a b
source
@[simp]
theorem set.Iio_diff_Iio {α : Type u_1} [linear_order α] {a b : α} :
set.Iio b \ set.Iio a = set.Ico a b
source
theorem set.Ioi_injective {α : Type u_1} [linear_order α] :
function.injective set.Ioi
source
theorem set.Iio_injective {α : Type u_1} [linear_order α] :
function.injective set.Iio
source
theorem set.Ioi_inj {α : Type u_1} [linear_order α] {a b : α} :
set.Ioi a = set.Ioi b ↔ a = b
source
theorem set.Iio_inj {α : Type u_1} [linear_order α] {a b : α} :
set.Iio a = set.Iio b ↔ a = b
source
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₂
source
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₁
source
theorem set.Ioo_subset_Ioo_iff {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} [densely_ordered α] (h₁ : a₁ < b₁) :
set.Ioo a₁ b₁ ⊆ set.Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
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₂
source
@[simp]
theorem set.Ioi_subset_Ioi_iff {α : Type u_1} [linear_order α] {a b : α} :
set.Ioi b ⊆ set.Ioi a ↔ a ≤ b
source
@[simp]
theorem set.Ioi_subset_Ici_iff {α : Type u_1} [linear_order α] {a b : α} [densely_ordered α] :
set.Ioi b ⊆ set.Ici a ↔ a ≤ b
source
@[simp]
theorem set.Iio_subset_Iio_iff {α : Type u_1} [linear_order α] {a b : α} :
set.Iio a ⊆ set.Iio b ↔ a ≤ b
source
@[simp]
theorem set.Iio_subset_Iic_iff {α : Type u_1} [linear_order α] {a b : α} [densely_ordered α] :
set.Iio a ⊆ set.Iic b ↔ a ≤ b

Unions of adjacent intervals #

Two infinite intervals #

source
theorem set.Iic_union_Ioi_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a ≤ b) :
set.Iic b ∪ set.Ioi a = set.univ
source
theorem set.Iio_union_Ici_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a ≤ b) :
set.Iio b ∪ set.Ici a = set.univ
source
theorem set.Iic_union_Ici_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a ≤ b) :
set.Iic b ∪ set.Ici a = set.univ
source
theorem set.Iio_union_Ioi_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
set.Iio b ∪ set.Ioi a = set.univ
source
@[simp]
theorem set.Iic_union_Ici {α : Type u_1} [linear_order α] {a : α} :
set.Iic a ∪ set.Ici a = set.univ
source
@[simp]
theorem set.Iio_union_Ici {α : Type u_1} [linear_order α] {a : α} :
set.Iio a ∪ set.Ici a = set.univ
source
@[simp]
theorem set.Iic_union_Ioi {α : Type u_1} [linear_order α] {a : α} :
set.Iic a ∪ set.Ioi a = set.univ
source
@[simp]
theorem set.Iio_union_Ioi {α : Type u_1} [linear_order α] {a : α} :
set.Iio a ∪ set.Ioi a = {a}ᶜ

A finite and an infinite interval #

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

An infinite and a finite interval #

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

Two finite intervals, I?o and Ic? #

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

Two finite intervals, I?c and Io? #

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

Two finite intervals with a common point #

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

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

source
theorem set.Ioc_subset_Ioc_union_Icc {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a c ⊆ set.Ioc a b ∪ set.Icc b c
source
@[simp]
theorem set.Ioc_union_Icc_eq_Ioc {α : Type u_1} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) :
set.Ioc a b ∪ set.Icc b c = set.Ioc a c
source
theorem set.Ioo_union_Ioo' {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : c < b) (h₂ : a < d) :
set.Ioo a b ∪ set.Ioo c d = set.Ioo (linear_order.min a c) (linear_order.max b d)
source
theorem set.Ioo_union_Ioo {α : Type u_1} [linear_order α] {a b c d : α} (h₁ : linear_order.min a b < linear_order.max c d) (h₂ : linear_order.min c d < linear_order.max a b) :
set.Ioo a b ∪ set.Ioo c d = set.Ioo (linear_order.min a c) (linear_order.max b d)
source
theorem monotone_on.image_Icc_subset {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} [lattice β] {f : α → β} (hf : monotone_on f (set.Icc a b)) :
f '' set.Icc a b ⊆ set.Icc (f a) (f b)
source
theorem antitone_on.image_Icc_subset {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} [lattice β] {f : α → β} (hf : antitone_on f (set.Icc a b)) :
f '' set.Icc a b ⊆ set.Icc (f b) (f a)
source
theorem monotone.image_Icc_subset {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} [lattice β] {f : α → β} (hf : monotone f) :
f '' set.Icc a b ⊆ set.Icc (f a) (f b)
source
theorem antitone.image_Icc_subset {α : Type u_1} {β : Type u_2} [linear_order α] {a b : α} [lattice β] {f : α → β} (hf : antitone f) :
f '' set.Icc a b ⊆ set.Icc (f b) (f a)
source
@[simp]
theorem set.Iic_inter_Iic {α : Type u_1} [semilattice_inf α] {a b : α} :
set.Iic a ∩ set.Iic b = set.Iic (a ⊓ b)
source
@[simp]
theorem set.Ioc_inter_Iic {α : Type u_1} [semilattice_inf α] (a b c : α) :
set.Ioc a b ∩ set.Iic c = set.Ioc a (b ⊓ c)
source
@[simp]
theorem set.Ici_inter_Ici {α : Type u_1} [semilattice_sup α] {a b : α} :
set.Ici a ∩ set.Ici b = set.Ici (a ⊔ b)
source
@[simp]
theorem set.Ico_inter_Ici {α : Type u_1} [semilattice_sup α] (a b c : α) :
set.Ico a b ∩ set.Ici c = set.Ico (a ⊔ c) b
source
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₂)
source
@[simp]
theorem set.Icc_inter_Icc_eq_singleton {α : Type u_1} [lattice α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
set.Icc a b ∩ set.Icc b c = {b}
source
@[simp]
theorem set.Ioi_inter_Ioi {α : Type u_1} [linear_order α] {a b : α} :
set.Ioi a ∩ set.Ioi b = set.Ioi (a ⊔ b)
source
@[simp]
theorem set.Iio_inter_Iio {α : Type u_1} [linear_order α] {a b : α} :
set.Iio a ∩ set.Iio b = set.Iio (a ⊓ b)
source
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₂)
source
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₂)
source
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₂)
source
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 (linear_order.max a₁ a₂) b₁
source
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 (linear_order.max a₁ a₂) b₂
source
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 (linear_order.max a₁ a₂) b₁
source
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 (linear_order.max a₁ a₂) b₂
source
@[simp]
theorem set.Ico_diff_Iio {α : Type u_1} [linear_order α] {a b c : α} :
set.Ico a b \ set.Iio c = set.Ico (linear_order.max a c) b
source
@[simp]
theorem set.Ioc_diff_Ioi {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a b \ set.Ioi c = set.Ioc a (linear_order.min b c)
source
@[simp]
theorem set.Ioc_inter_Ioi {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a b ∩ set.Ioi c = set.Ioc (a ⊔ c) b
source
@[simp]
theorem set.Ico_inter_Iio {α : Type u_1} [linear_order α] {a b c : α} :
set.Ico a b ∩ set.Iio c = set.Ico a (linear_order.min b c)
source
@[simp]
theorem set.Ioc_diff_Iic {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a b \ set.Iic c = set.Ioc (linear_order.max a c) b
source
@[simp]
theorem set.Ioc_union_Ioc_right {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a b ∪ set.Ioc a c = set.Ioc a (linear_order.max b c)
source
@[simp]
theorem set.Ioc_union_Ioc_left {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a c ∪ set.Ioc b c = set.Ioc (linear_order.min a b) c
source
@[simp]
theorem set.Ioc_union_Ioc_symm {α : Type u_1} [linear_order α] {a b : α} :
set.Ioc a b ∪ set.Ioc b a = set.Ioc (linear_order.min a b) (linear_order.max a b)
source
@[simp]
theorem set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u_1} [linear_order α] {a b c : α} :
set.Ioc a b ∪ set.Ioc b c ∪ set.Ioc c a = set.Ioc (linear_order.min a (linear_order.min b c)) (linear_order.max a (linear_order.max b c))

Closed intervals in α × β #

source
@[simp]
theorem set.Iic_prod_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
set.Iic a ×ˢ set.Iic b = set.Iic (a, b)
source
@[simp]
theorem set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
set.Ici a ×ˢ set.Ici b = set.Ici (a, b)
source
theorem set.Ici_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α × β) :
set.Ici a = set.Ici a.fst ×ˢ set.Ici a.snd
source
theorem set.Iic_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α × β) :
set.Iic a = set.Iic a.fst ×ˢ set.Iic a.snd
source
@[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₂)
source
theorem set.Icc_prod_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a b : α × β) :
set.Icc a b = set.Icc a.fst b.fst ×ˢ set.Icc a.snd b.snd

Lemmas about intervals in dense orders #

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