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

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

Left-open right-open interval

Equations
source
def set.Ico {α : Type u} [preorder α] (a b : α) :
set α

Left-closed right-open interval

Equations
source
def set.Iio {α : Type u} [preorder α] (a : α) :
set α

Left-infinite right-open interval

Equations
source
def set.Icc {α : Type u} [preorder α] (a b : α) :
set α

Left-closed right-closed interval

Equations
source
def set.Iic {α : Type u} [preorder α] (b : α) :
set α

Left-infinite right-closed interval

Equations
source
def set.Ioc {α : Type u} [preorder α] (a b : α) :
set α

Left-open right-closed interval

Equations
source
def set.Ici {α : Type u} [preorder α] (a : α) :
set α

Left-closed right-infinite interval

Equations
source
def set.Ioi {α : Type u} [preorder α] (a : α) :
set α

Left-open right-infinite interval

Equations
source
theorem set.Ioo_def {α : Type u} [preorder α] (a b : α) :
{x : α | a < x ∧ x < b} = set.Ioo a b
source
theorem set.Ico_def {α : Type u} [preorder α] (a b : α) :
{x : α | a ≤ x ∧ x < b} = set.Ico a b
source
theorem set.Iio_def {α : Type u} [preorder α] (a : α) :
{x : α | x < a} = set.Iio a
source
theorem set.Icc_def {α : Type u} [preorder α] (a b : α) :
{x : α | a ≤ x ∧ x ≤ b} = set.Icc a b
source
theorem set.Iic_def {α : Type u} [preorder α] (b : α) :
{x : α | x ≤ b} = set.Iic b
source
theorem set.Ioc_def {α : Type u} [preorder α] (a b : α) :
{x : α | a < x ∧ x ≤ b} = set.Ioc a b
source
theorem set.Ici_def {α : Type u} [preorder α] (a : α) :
{x : α | a ≤ x} = set.Ici a
source
theorem set.Ioi_def {α : Type u} [preorder α] (a : α) :
{x : α | a < x} = set.Ioi a
source
@[simp]
theorem set.mem_Ioo {α : Type u} [preorder α] {a b x : α} :
x ∈ set.Ioo a b ↔ a < x ∧ x < b
source
@[simp]
theorem set.mem_Ico {α : Type u} [preorder α] {a b x : α} :
x ∈ set.Ico a b ↔ a ≤ x ∧ x < b
source
@[simp]
theorem set.mem_Iio {α : Type u} [preorder α] {b x : α} :
x ∈ set.Iio b ↔ x < b
source
@[simp]
theorem set.mem_Icc {α : Type u} [preorder α] {a b x : α} :
x ∈ set.Icc a b ↔ a ≤ x ∧ x ≤ b
source
@[simp]
theorem set.mem_Iic {α : Type u} [preorder α] {b x : α} :
x ∈ set.Iic b ↔ x ≤ b
source
@[simp]
theorem set.mem_Ioc {α : Type u} [preorder α] {a b x : α} :
x ∈ set.Ioc a b ↔ a < x ∧ x ≤ b
source
@[simp]
theorem set.mem_Ici {α : Type u} [preorder α] {a x : α} :
x ∈ set.Ici a ↔ a ≤ x
source
@[simp]
theorem set.mem_Ioi {α : Type u} [preorder α] {a x : α} :
x ∈ set.Ioi a ↔ a < x
source
@[simp]
theorem set.left_mem_Ioo {α : Type u} [preorder α] {a b : α} :
a ∈ set.Ioo a b ↔ false
source
@[simp]
theorem set.left_mem_Ico {α : Type u} [preorder α] {a b : α} :
a ∈ set.Ico a b ↔ a < b
source
@[simp]
theorem set.left_mem_Icc {α : Type u} [preorder α] {a b : α} :
a ∈ set.Icc a b ↔ a ≤ b
source
@[simp]
theorem set.left_mem_Ioc {α : Type u} [preorder α] {a b : α} :
a ∈ set.Ioc a b ↔ false
source
theorem set.left_mem_Ici {α : Type u} [preorder α] {a : α} :
a ∈ set.Ici a
source
@[simp]
theorem set.right_mem_Ioo {α : Type u} [preorder α] {a b : α} :
b ∈ set.Ioo a b ↔ false
source
@[simp]
theorem set.right_mem_Ico {α : Type u} [preorder α] {a b : α} :
b ∈ set.Ico a b ↔ false
source
@[simp]
theorem set.right_mem_Icc {α : Type u} [preorder α] {a b : α} :
b ∈ set.Icc a b ↔ a ≤ b
source
@[simp]
theorem set.right_mem_Ioc {α : Type u} [preorder α] {a b : α} :
b ∈ set.Ioc a b ↔ a < b
source
theorem set.right_mem_Iic {α : Type u} [preorder α] {a : α} :
a ∈ set.Iic a
source
@[simp]
theorem set.dual_Ici {α : Type u} [preorder α] {a : α} :
set.Ici (⇑order_dual.to_dual a) = ⇑order_dual.of_dual ⁻¹' set.Iic a
source
@[simp]
theorem set.dual_Iic {α : Type u} [preorder α] {a : α} :
set.Iic (⇑order_dual.to_dual a) = ⇑order_dual.of_dual ⁻¹' set.Ici a
source
@[simp]
theorem set.dual_Ioi {α : Type u} [preorder α] {a : α} :
set.Ioi (⇑order_dual.to_dual a) = ⇑order_dual.of_dual ⁻¹' set.Iio a
source
@[simp]
theorem set.dual_Iio {α : Type u} [preorder α] {a : α} :
set.Iio (⇑order_dual.to_dual a) = ⇑order_dual.of_dual ⁻¹' set.Ioi a
source
@[simp]
theorem set.dual_Icc {α : Type u} [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} [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} [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} [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} [preorder α] {a b : α} :
(set.Icc a b).nonempty ↔ a ≤ b
source
@[simp]
theorem set.nonempty_Ico {α : Type u} [preorder α] {a b : α} :
(set.Ico a b).nonempty ↔ a < b
source
@[simp]
theorem set.nonempty_Ioc {α : Type u} [preorder α] {a b : α} :
(set.Ioc a b).nonempty ↔ a < b
source
@[simp]
theorem set.nonempty_Ici {α : Type u} [preorder α] {a : α} :
(set.Ici a).nonempty
source
@[simp]
theorem set.nonempty_Iic {α : Type u} [preorder α] {a : α} :
(set.Iic a).nonempty
source
@[simp]
theorem set.nonempty_Ioo {α : Type u} [preorder α] {a b : α} [densely_ordered α] :
(set.Ioo a b).nonempty ↔ a < b
source
@[simp]
theorem set.nonempty_Ioi {α : Type u} [preorder α] {a : α} [no_top_order α] :
(set.Ioi a).nonempty
source
@[simp]
theorem set.nonempty_Iio {α : Type u} [preorder α] {a : α} [no_bot_order α] :
(set.Iio a).nonempty
source
theorem set.nonempty_Icc_subtype {α : Type u} [preorder α] {a b : α} (h : a ≤ b) :
nonempty ↥(set.Icc a b)
source
theorem set.nonempty_Ico_subtype {α : Type u} [preorder α] {a b : α} (h : a < b) :
nonempty ↥(set.Ico a b)
source
theorem set.nonempty_Ioc_subtype {α : Type u} [preorder α] {a b : α} (h : a < b) :
nonempty ↥(set.Ioc a b)
source
@[protected, instance]
def set.nonempty_Ici_subtype {α : Type u} [preorder α] {a : α} :
nonempty ↥(set.Ici a)

An interval Ici a is nonempty.

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

An interval Iic a is nonempty.

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

In a no_top_order, the intervals Ioi are nonempty.

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

In a no_bot_order, the intervals Iio are nonempty.

source
@[simp]
theorem set.Icc_eq_empty {α : Type u} [preorder α] {a b : α} (h : ¬a ≤ b) :
set.Icc a b = ∅
source
@[simp]
theorem set.Ico_eq_empty {α : Type u} [preorder α] {a b : α} (h : ¬a < b) :
set.Ico a b = ∅
source
@[simp]
theorem set.Ioc_eq_empty {α : Type u} [preorder α] {a b : α} (h : ¬a < b) :
set.Ioc a b = ∅
source
@[simp]
theorem set.Ioo_eq_empty {α : Type u} [preorder α] {a b : α} (h : ¬a < b) :
set.Ioo a b = ∅
source
@[simp]
theorem set.Icc_eq_empty_of_lt {α : Type u} [preorder α] {a b : α} (h : b < a) :
set.Icc a b = ∅
source
@[simp]
theorem set.Ico_eq_empty_of_le {α : Type u} [preorder α] {a b : α} (h : b ≤ a) :
set.Ico a b = ∅
source
@[simp]
theorem set.Ioc_eq_empty_of_le {α : Type u} [preorder α] {a b : α} (h : b ≤ a) :
set.Ioc a b = ∅
source
@[simp]
theorem set.Ioo_eq_empty_of_le {α : Type u} [preorder α] {a b : α} (h : b ≤ a) :
set.Ioo a b = ∅
source
@[simp]
theorem set.Ico_self {α : Type u} [preorder α] (a : α) :
set.Ico a a = ∅
source
@[simp]
theorem set.Ioc_self {α : Type u} [preorder α] (a : α) :
set.Ioc a a = ∅
source
@[simp]
theorem set.Ioo_self {α : Type u} [preorder α] (a : α) :
set.Ioo a a = ∅
source
theorem set.Ici_subset_Ici {α : Type u} [preorder α] {a b : α} :
set.Ici a ⊆ set.Ici b ↔ b ≤ a
source
theorem set.Iic_subset_Iic {α : Type u} [preorder α] {a b : α} :
set.Iic a ⊆ set.Iic b ↔ a ≤ b
source
theorem set.Ici_subset_Ioi {α : Type u} [preorder α] {a b : α} :
set.Ici a ⊆ set.Ioi b ↔ b < a
source
theorem set.Iic_subset_Iio {α : Type u} [preorder α] {a b : α} :
set.Iic a ⊆ set.Iio b ↔ a < b
source
theorem set.Ioo_subset_Ioo {α : Type u} [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} [preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
set.Ioo a₂ b ⊆ set.Ioo a₁ b
source
theorem set.Ioo_subset_Ioo_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
set.Ioo a b₁ ⊆ set.Ioo a b₂
source
theorem set.Ico_subset_Ico {α : Type u} [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} [preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
set.Ico a₂ b ⊆ set.Ico a₁ b
source
theorem set.Ico_subset_Ico_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
set.Ico a b₁ ⊆ set.Ico a b₂
source
theorem set.Icc_subset_Icc {α : Type u} [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} [preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
set.Icc a₂ b ⊆ set.Icc a₁ b
source
theorem set.Icc_subset_Icc_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
set.Icc a b₁ ⊆ set.Icc a b₂
source
theorem set.Icc_subset_Ioo {α : Type u} [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} [preorder α] {a b : α} :
set.Icc a b ⊆ set.Ici a
source
theorem set.Icc_subset_Iic_self {α : Type u} [preorder α] {a b : α} :
set.Icc a b ⊆ set.Iic b
source
theorem set.Ioc_subset_Iic_self {α : Type u} [preorder α] {a b : α} :
set.Ioc a b ⊆ set.Iic b
source
theorem set.Ioc_subset_Ioc {α : Type u} [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} [preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
set.Ioc a₂ b ⊆ set.Ioc a₁ b
source
theorem set.Ioc_subset_Ioc_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
set.Ioc a b₁ ⊆ set.Ioc a b₂
source
theorem set.Ico_subset_Ioo_left {α : Type u} [preorder α] {a₁ a₂ b : α} (h₁ : a₁ < a₂) :
set.Ico a₂ b ⊆ set.Ioo a₁ b
source
theorem set.Ioc_subset_Ioo_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
set.Ioc a b₁ ⊆ set.Ioo a b₂
source
theorem set.Icc_subset_Ico_right {α : Type u} [preorder α] {a b₁ b₂ : α} (h₁ : b₁ < b₂) :
set.Icc a b₁ ⊆ set.Ico a b₂
source
theorem set.Ioo_subset_Ico_self {α : Type u} [preorder α] {a b : α} :
set.Ioo a b ⊆ set.Ico a b
source
theorem set.Ioo_subset_Ioc_self {α : Type u} [preorder α] {a b : α} :
set.Ioo a b ⊆ set.Ioc a b
source
theorem set.Ico_subset_Icc_self {α : Type u} [preorder α] {a b : α} :
set.Ico a b ⊆ set.Icc a b
source
theorem set.Ioc_subset_Icc_self {α : Type u} [preorder α] {a b : α} :
set.Ioc a b ⊆ set.Icc a b
source
theorem set.Ioo_subset_Icc_self {α : Type u} [preorder α] {a b : α} :
set.Ioo a b ⊆ set.Icc a b
source
theorem set.Ico_subset_Iio_self {α : Type u} [preorder α] {a b : α} :
set.Ico a b ⊆ set.Iio b
source
theorem set.Ioo_subset_Iio_self {α : Type u} [preorder α] {a b : α} :
set.Ioo a b ⊆ set.Iio b
source
theorem set.Ioc_subset_Ioi_self {α : Type u} [preorder α] {a b : α} :
set.Ioc a b ⊆ set.Ioi a
source
theorem set.Ioo_subset_Ioi_self {α : Type u} [preorder α] {a b : α} :
set.Ioo a b ⊆ set.Ioi a
source
theorem set.Ioi_subset_Ici_self {α : Type u} [preorder α] {a : α} :
set.Ioi a ⊆ set.Ici a
source
theorem set.Iio_subset_Iic_self {α : Type u} [preorder α] {a : α} :
set.Iio a ⊆ set.Iic a
source
theorem set.Ico_subset_Ici_self {α : Type u} [preorder α] {a b : α} :
set.Ico a b ⊆ set.Ici a
source
theorem set.Icc_subset_Icc_iff {α : Type u} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [preorder α] {a b : α} :
set.Ici a ∩ set.Iic b = set.Icc a b
source
theorem set.Ici_inter_Iio {α : Type u} [preorder α] {a b : α} :
set.Ici a ∩ set.Iio b = set.Ico a b
source
theorem set.Ioi_inter_Iic {α : Type u} [preorder α] {a b : α} :
set.Ioi a ∩ set.Iic b = set.Ioc a b
source
theorem set.Ioi_inter_Iio {α : Type u} [preorder α] {a b : α} :
set.Ioi a ∩ set.Iio b = set.Ioo a b
source
theorem set.mem_Icc_of_Ioo {α : Type u} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Icc a b
source
theorem set.mem_Ico_of_Ioo {α : Type u} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Ico a b
source
theorem set.mem_Ioc_of_Ioo {α : Type u} [preorder α] {a b x : α} (h : x ∈ set.Ioo a b) :
x ∈ set.Ioc a b
source
theorem set.mem_Icc_of_Ico {α : Type u} [preorder α] {a b x : α} (h : x ∈ set.Ico a b) :
x ∈ set.Icc a b
source
theorem set.mem_Icc_of_Ioc {α : Type u} [preorder α] {a b x : α} (h : x ∈ set.Ioc a b) :
x ∈ set.Icc a b
source
theorem set.mem_Ici_of_Ioi {α : Type u} [preorder α] {a x : α} (h : x ∈ set.Ioi a) :
x ∈ set.Ici a
source
theorem set.mem_Iic_of_Iio {α : Type u} [preorder α] {a x : α} (h : x ∈ set.Iio a) :
x ∈ set.Iic a
source
theorem set.Icc_eq_empty_iff {α : Type u} [preorder α] {a b : α} :
set.Icc a b = ∅ ↔ ¬a ≤ b
source
theorem set.Ico_eq_empty_iff {α : Type u} [preorder α] {a b : α} :
set.Ico a b = ∅ ↔ ¬a < b
source
theorem set.Ioc_eq_empty_iff {α : Type u} [preorder α] {a b : α} :
set.Ioc a b = ∅ ↔ ¬a < b
source
theorem set.Ioo_eq_empty_iff {α : Type u} [preorder α] {a b : α} [densely_ordered α] :
set.Ioo a b = ∅ ↔ ¬a < b
source
@[simp]
theorem set.Icc_self {α : Type u} [partial_order α] (a : α) :
set.Icc a a = {a}
source
@[simp]
theorem set.Icc_eq_singleton_iff {α : Type u} [partial_order α] {a b c : α} :
set.Icc a b = {c} ↔ a = c ∧ b = c
source
@[simp]
theorem set.Icc_diff_left {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {a} = set.Ioc a b
source
@[simp]
theorem set.Icc_diff_right {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {b} = set.Ico a b
source
@[simp]
theorem set.Ico_diff_left {α : Type u} [partial_order α] {a b : α} :
set.Ico a b \ {a} = set.Ioo a b
source
@[simp]
theorem set.Ioc_diff_right {α : Type u} [partial_order α] {a b : α} :
set.Ioc a b \ {b} = set.Ioo a b
source
@[simp]
theorem set.Icc_diff_both {α : Type u} [partial_order α] {a b : α} :
set.Icc a b \ {a, b} = set.Ioo a b
source
@[simp]
theorem set.Ici_diff_left {α : Type u} [partial_order α] {a : α} :
set.Ici a \ {a} = set.Ioi a
source
@[simp]
theorem set.Iic_diff_right {α : Type u} [partial_order α] {a : α} :
set.Iic a \ {a} = set.Iio a
source
@[simp]
theorem set.Ico_diff_Ioo_same {α : Type u} [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} [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} [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} [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} [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} [partial_order α] {a : α} :
set.Ici a \ set.Ioi a = {a}
source
@[simp]
theorem set.Iic_diff_Iio_same {α : Type u} [partial_order α] {a : α} :
set.Iic a \ set.Iio a = {a}
source
@[simp]
theorem set.Ioi_union_left {α : Type u} [partial_order α] {a : α} :
set.Ioi a ∪ {a} = set.Ici a
source
@[simp]
theorem set.Iio_union_right {α : Type u} [partial_order α] {a : α} :
set.Iio a ∪ {a} = set.Iic a
source
theorem set.Ioo_union_left {α : Type u} [partial_order α] {a b : α} (hab : a < b) :
set.Ioo a b ∪ {a} = set.Ico a b
source
theorem set.Ioo_union_right {α : Type u} [partial_order α] {a b : α} (hab : a < b) :
set.Ioo a b ∪ {b} = set.Ioc a b
source
theorem set.Ioc_union_left {α : Type u} [partial_order α] {a b : α} (hab : a ≤ b) :
set.Ioc a b ∪ {a} = set.Icc a b
source
theorem set.Ico_union_right {α : Type u} [partial_order α] {a b : α} (hab : a ≤ b) :
set.Ico a b ∪ {b} = set.Icc a b
source
theorem set.mem_Ici_Ioi_of_subset_of_subset {α : Type u} [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} [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} [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.mem_Ioo_or_eq_endpoints_of_mem_Icc {α : Type u} [partial_order α] {a b x : α} (hmem : x ∈ set.Icc a b) :
x = a ∨ x = b ∨ x ∈ set.Ioo a b
source
theorem set.mem_Ioo_or_eq_left_of_mem_Ico {α : Type u} [partial_order α] {a b x : α} (hmem : x ∈ set.Ico a b) :
x = a ∨ x ∈ set.Ioo a b
source
theorem set.mem_Ioo_or_eq_right_of_mem_Ioc {α : Type u} [partial_order α] {a b x : α} (hmem : x ∈ set.Ioc a b) :
x = b ∨ x ∈ set.Ioo a b
source
theorem set.Ici_singleton_of_top {α : Type u} [partial_order α] {a : α} (h_top : ∀ (x : α), x ≤ a) :
set.Ici a = {a}
source
theorem set.Iic_singleton_of_bot {α : Type u} [partial_order α] {a : α} (h_bot : ∀ (x : α), a ≤ x) :
set.Iic a = {a}
source
theorem set.Iic_inter_Ioc_of_le {α : Type u} [partial_order α] {a b c : α} (h : a ≤ c) :
set.Iic a ∩ set.Ioc b c = set.Ioc b a
source
@[simp]
theorem set.Ici_top {α : Type u} [partial_order α] [order_top α] :
set.Ici ⊤ = {⊤}
source
@[simp]
theorem set.Iic_top {α : Type u} [preorder α] [order_top α] :
set.Iic ⊤ = set.univ
source
@[simp]
theorem set.Icc_top {α : Type u} [preorder α] [order_top α] {a : α} :
set.Icc a ⊤ = set.Ici a
source
@[simp]
theorem set.Ioc_top {α : Type u} [preorder α] [order_top α] {a : α} :
set.Ioc a ⊤ = set.Ioi a
source
@[simp]
theorem set.Iic_bot {α : Type u} [partial_order α] [order_bot α] :
set.Iic ⊥ = {⊥}
source
@[simp]
theorem set.Ici_bot {α : Type u} [preorder α] [order_bot α] :
set.Ici ⊥ = set.univ
source
@[simp]
theorem set.Icc_bot {α : Type u} [preorder α] [order_bot α] {a : α} :
set.Icc ⊥ a = set.Iic a
source
@[simp]
theorem set.Ico_bot {α : Type u} [preorder α] [order_bot α] {a : α} :
set.Ico ⊥ a = set.Iio a
source
theorem set.not_mem_Ici {α : Type u} [linear_order α] {a c : α} :
c ∉ set.Ici a ↔ c < a
source
theorem set.not_mem_Iic {α : Type u} [linear_order α] {b c : α} :
c ∉ set.Iic b ↔ b < c
source
theorem set.not_mem_Icc_of_lt {α : Type u} [linear_order α] {a b c : α} (ha : c < a) :
c ∉ set.Icc a b
source
theorem set.not_mem_Icc_of_gt {α : Type u} [linear_order α] {a b c : α} (hb : b < c) :
c ∉ set.Icc a b
source
theorem set.not_mem_Ico_of_lt {α : Type u} [linear_order α] {a b c : α} (ha : c < a) :
c ∉ set.Ico a b
source
theorem set.not_mem_Ioc_of_gt {α : Type u} [linear_order α] {a b c : α} (hb : b < c) :
c ∉ set.Ioc a b
source
theorem set.not_mem_Ioi {α : Type u} [linear_order α] {a c : α} :
c ∉ set.Ioi a ↔ c ≤ a
source
theorem set.not_mem_Iio {α : Type u} [linear_order α] {b c : α} :
c ∉ set.Iio b ↔ b ≤ c
source
theorem set.not_mem_Ioc_of_le {α : Type u} [linear_order α] {a b c : α} (ha : c ≤ a) :
c ∉ set.Ioc a b
source
theorem set.not_mem_Ico_of_ge {α : Type u} [linear_order α] {a b c : α} (hb : b ≤ c) :
c ∉ set.Ico a b
source
theorem set.not_mem_Ioo_of_le {α : Type u} [linear_order α] {a b c : α} (ha : c ≤ a) :
c ∉ set.Ioo a b
source
theorem set.not_mem_Ioo_of_ge {α : Type u} [linear_order α] {a b c : α} (hb : b ≤ c) :
c ∉ set.Ioo a b
source
@[simp]
theorem set.compl_Iic {α : Type u} [linear_order α] {a : α} :
(set.Iic a)ᶜ = set.Ioi a
source
@[simp]
theorem set.compl_Ici {α : Type u} [linear_order α] {a : α} :
(set.Ici a)ᶜ = set.Iio a
source
@[simp]
theorem set.compl_Iio {α : Type u} [linear_order α] {a : α} :
(set.Iio a)ᶜ = set.Ici a
source
@[simp]
theorem set.compl_Ioi {α : Type u} [linear_order α] {a : α} :
(set.Ioi a)ᶜ = set.Iic a
source
@[simp]
theorem set.Ici_diff_Ici {α : Type u} [linear_order α] {a b : α} :
set.Ici a \ set.Ici b = set.Ico a b
source
@[simp]
theorem set.Ici_diff_Ioi {α : Type u} [linear_order α] {a b : α} :
set.Ici a \ set.Ioi b = set.Icc a b
source
@[simp]
theorem set.Ioi_diff_Ioi {α : Type u} [linear_order α] {a b : α} :
set.Ioi a \ set.Ioi b = set.Ioc a b
source
@[simp]
theorem set.Ioi_diff_Ici {α : Type u} [linear_order α] {a b : α} :
set.Ioi a \ set.Ici b = set.Ioo a b
source
@[simp]
theorem set.Iic_diff_Iic {α : Type u} [linear_order α] {a b : α} :
set.Iic b \ set.Iic a = set.Ioc a b
source
@[simp]
theorem set.Iio_diff_Iic {α : Type u} [linear_order α] {a b : α} :
set.Iio b \ set.Iic a = set.Ioo a b
source
@[simp]
theorem set.Iic_diff_Iio {α : Type u} [linear_order α] {a b : α} :
set.Iic b \ set.Iio a = set.Icc a b
source
@[simp]
theorem set.Iio_diff_Iio {α : Type u} [linear_order α] {a b : α} :
set.Iio b \ set.Iio a = set.Ico a b
source
theorem set.Ico_subset_Ico_iff {α : Type u} [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} [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} [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} [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} [linear_order α] {a b : α} :
set.Ioi b ⊆ set.Ioi a ↔ a ≤ b
source
@[simp]
theorem set.Ioi_subset_Ici_iff {α : Type u} [linear_order α] {a b : α} [densely_ordered α] :
set.Ioi b ⊆ set.Ici a ↔ a ≤ b
source
@[simp]
theorem set.Iio_subset_Iio_iff {α : Type u} [linear_order α] {a b : α} :
set.Iio a ⊆ set.Iio b ↔ a ≤ b
source
@[simp]
theorem set.Iio_subset_Iic_iff {α : Type u} [linear_order α] {a b : α} [densely_ordered α] :
set.Iio a ⊆ set.Iic b ↔ a ≤ b

Unions of adjacent intervals #

Two infinite intervals #

source
@[simp]
theorem set.Iic_union_Ici {α : Type u} [linear_order α] {a : α} :
set.Iic a ∪ set.Ici a = set.univ
source
@[simp]
theorem set.Iio_union_Ici {α : Type u} [linear_order α] {a : α} :
set.Iio a ∪ set.Ici a = set.univ
source
@[simp]
theorem set.Iic_union_Ioi {α : Type u} [linear_order α] {a : α} :
set.Iic a ∪ set.Ioi a = set.univ

A finite and an infinite interval #

source
theorem set.Ioo_union_Ioi' {α : Type u} [linear_order α] {a b c : α} (h₁ : c < b) :
set.Ioo a b ∪ set.Ioi c = set.Ioi (min a c)
source
theorem set.Ioo_union_Ioi {α : Type u} [linear_order α] {a b c : α} (h : c < max a b) :
set.Ioo a b ∪ set.Ioi c = set.Ioi (min a c)
source
theorem set.Ioi_subset_Ioo_union_Ici {α : Type u} [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} [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} [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} [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} [linear_order α] {a b c : α} (h₁ : c ≤ b) :
set.Ico a b ∪ set.Ici c = set.Ici (min a c)
source
theorem set.Ico_union_Ici {α : Type u} [linear_order α] {a b c : α} (h : c ≤ max a b) :
set.Ico a b ∪ set.Ici c = set.Ici (min a c)
source
theorem set.Ioi_subset_Ioc_union_Ioi {α : Type u} [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} [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} [linear_order α] {a b c : α} (h₁ : c ≤ b) :
set.Ioc a b ∪ set.Ioi c = set.Ioi (min a c)
source
theorem set.Ioc_union_Ioi {α : Type u} [linear_order α] {a b c : α} (h : c ≤ max a b) :
set.Ioc a b ∪ set.Ioi c = set.Ioi (min a c)
source
theorem set.Ici_subset_Icc_union_Ioi {α : Type u} [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} [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} [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} [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} [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} [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} [linear_order α] {a b c : α} (h₁ : c ≤ b) :
set.Icc a b ∪ set.Ici c = set.Ici (min a c)
source
theorem set.Icc_union_Ici {α : Type u} [linear_order α] {a b c : α} (h : c ≤ max a b) :
set.Icc a b ∪ set.Ici c = set.Ici (min a c)

An infinite and a finite interval #

source
theorem set.Iic_subset_Iio_union_Icc {α : Type u} [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} [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} [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} [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} [linear_order α] {b c d : α} (h₁ : c ≤ b) :
set.Iio b ∪ set.Ico c d = set.Iio (max b d)
source
theorem set.Iio_union_Ico {α : Type u} [linear_order α] {b c d : α} (h : min c d ≤ b) :
set.Iio b ∪ set.Ico c d = set.Iio (max b d)
source
theorem set.Iic_subset_Iic_union_Ioc {α : Type u} [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} [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} [linear_order α] {b c d : α} (h₁ : c < b) :
set.Iic b ∪ set.Ioc c d = set.Iic (max b d)
source
theorem set.Iic_union_Ioc {α : Type u} [linear_order α] {b c d : α} (h : min c d < b) :
set.Iic b ∪ set.Ioc c d = set.Iic (max b d)
source
theorem set.Iio_subset_Iic_union_Ioo {α : Type u} [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} [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} [linear_order α] {b c d : α} (h₁ : c < b) :
set.Iio b ∪ set.Ioo c d = set.Iio (max b d)
source
theorem set.Iio_union_Ioo {α : Type u} [linear_order α] {b c d : α} (h : min c d < b) :
set.Iio b ∪ set.Ioo c d = set.Iio (max b d)
source
theorem set.Iic_subset_Iic_union_Icc {α : Type u} [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} [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} [linear_order α] {b c d : α} (h₁ : c ≤ b) :
set.Iic b ∪ set.Icc c d = set.Iic (max b d)
source
theorem set.Iic_union_Icc {α : Type u} [linear_order α] {b c d : α} (h : min c d ≤ b) :
set.Iic b ∪ set.Icc c d = set.Iic (max b d)
source
theorem set.Iio_subset_Iic_union_Ico {α : Type u} [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} [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} [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} [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} [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} [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} [linear_order α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
set.Ico a b ∪ set.Ico c d = set.Ico (min a c) (max b d)
source
theorem set.Ico_union_Ico {α : Type u} [linear_order α] {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
set.Ico a b ∪ set.Ico c d = set.Ico (min a c) (max b d)
source
theorem set.Icc_subset_Ico_union_Icc {α : Type u} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [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} [linear_order α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
set.Ioc a b ∪ set.Ioc c d = set.Ioc (min a c) (max b d)
source
theorem set.Ioc_union_Ioc {α : Type u} [linear_order α] {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
set.Ioc a b ∪ set.Ioc c d = set.Ioc (min a c) (max b d)

Two finite intervals with a common point #

source
theorem set.Ioo_subset_Ioc_union_Ico {α : Type u} [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} [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} [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} [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} [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} [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} [linear_order α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) :
set.Icc a b ∪ set.Icc c d = set.Icc (min a c) (max b d)
source
theorem set.Icc_union_Icc {α : Type u} [linear_order α] {a b c d : α} (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
set.Icc a b ∪ set.Icc c d = set.Icc (min a c) (max b d)

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

source
theorem set.Ioc_subset_Ioc_union_Icc {α : Type u} [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} [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} [linear_order α] {a b c d : α} (h₁ : c < b) (h₂ : a < d) :
set.Ioo a b ∪ set.Ioo c d = set.Ioo (min a c) (max b d)
source
theorem set.Ioo_union_Ioo {α : Type u} [linear_order α] {a b c d : α} (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
set.Ioo a b ∪ set.Ioo c d = set.Ioo (min a c) (max b d)
source
@[simp]
theorem set.Iic_inter_Iic {α : Type u} [semilattice_inf α] {a b : α} :
set.Iic a ∩ set.Iic b = set.Iic (a ⊓ b)
source
@[simp]
theorem set.Iio_inter_Iio {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b : α} :
set.Iio a ∩ set.Iio b = set.Iio (a ⊓ b)
source
@[simp]
theorem set.Ioc_inter_Iic {α : Type u} [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} [semilattice_sup α] {a b : α} :
set.Ici a ∩ set.Ici b = set.Ici (a ⊔ b)
source
@[simp]
theorem set.Ico_inter_Ici {α : Type u} [semilattice_sup α] (a b c : α) :
set.Ico a b ∩ set.Ici c = set.Ico (a ⊔ c) b
source
@[simp]
theorem set.Ioi_inter_Ioi {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b : α} :
set.Ioi a ∩ set.Ioi b = set.Ioi (a ⊔ b)
source
@[simp]
theorem set.Ioc_inter_Ioi {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
set.Ioc a b ∩ set.Ioi c = set.Ioc (a ⊔ c) b
source
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₂)
source
@[simp]
theorem set.Icc_inter_Icc_eq_singleton {α : Type u} [lattice α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
set.Icc a b ∩ set.Icc b c = {b}
source
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₂)
source
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₂)
source
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₂)
source
theorem set.Icc_bot_top {α : Type u_1} [partial_order α] [bounded_order α] :
set.Icc ⊥ ⊤ = set.univ
source
theorem set.Ioc_inter_Ioo_of_left_lt {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₁ < b₂) :
set.Ioc a₁ b₁ ∩ set.Ioo a₂ b₂ = set.Ioc (max a₁ a₂) b₁
source
theorem set.Ioc_inter_Ioo_of_right_le {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₂ ≤ b₁) :
set.Ioc a₁ b₁ ∩ set.Ioo a₂ b₂ = set.Ioo (max a₁ a₂) b₂
source
theorem set.Ioo_inter_Ioc_of_left_le {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₁ ≤ b₂) :
set.Ioo a₁ b₁ ∩ set.Ioc a₂ b₂ = set.Ioo (max a₁ a₂) b₁
source
theorem set.Ioo_inter_Ioc_of_right_lt {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h : b₂ < b₁) :
set.Ioo a₁ b₁ ∩ set.Ioc a₂ b₂ = set.Ioc (max a₁ a₂) b₂
source
@[simp]
theorem set.Ico_diff_Iio {α : Type u} [linear_order α] {a b c : α} :
set.Ico a b \ set.Iio c = set.Ico (max a c) b
source
@[simp]
theorem set.Ioc_diff_Ioi {α : Type u} [linear_order α] {a b c : α} :
set.Ioc a b \ set.Ioi c = set.Ioc a (min b c)
source
@[simp]
theorem set.Ico_inter_Iio {α : Type u} [linear_order α] {a b c : α} :
set.Ico a b ∩ set.Iio c = set.Ico a (min b c)
source
@[simp]
theorem set.Ioc_diff_Iic {α : Type u} [linear_order α] {a b c : α} :
set.Ioc a b \ set.Iic c = set.Ioc (max a c) b
source
@[simp]
theorem set.Ioc_union_Ioc_right {α : Type u} [linear_order α] {a b c : α} :
set.Ioc a b ∪ set.Ioc a c = set.Ioc a (max b c)
source
@[simp]
theorem set.Ioc_union_Ioc_left {α : Type u} [linear_order α] {a b c : α} :
set.Ioc a c ∪ set.Ioc b c = set.Ioc (min a b) c
source
@[simp]
theorem set.Ioc_union_Ioc_symm {α : Type u} [linear_order α] {a b : α} :
set.Ioc a b ∪ set.Ioc b a = set.Ioc (min a b) (max a b)
source
@[simp]
theorem set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u} [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))

Closed intervals in α × β #

source
@[simp]
theorem set.Iic_prod_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
(set.Iic a).prod (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).prod (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).prod (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).prod (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₂).prod (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).prod (set.Icc a.snd b.snd)

Lemmas about membership of arithmetic operations #

inv_mem_Ixx_iff, sub_mem_Ixx_iff

source
theorem set.neg_mem_Icc_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a ∈ set.Icc c d ↔ a ∈ set.Icc (-d) (-c)
source
theorem set.inv_mem_Icc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
a⁻¹ ∈ set.Icc c d ↔ a ∈ set.Icc d⁻¹ c⁻¹
source
theorem set.neg_mem_Ico_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a ∈ set.Ico c d ↔ a ∈ set.Ioc (-d) (-c)
source
theorem set.inv_mem_Ico_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
a⁻¹ ∈ set.Ico c d ↔ a ∈ set.Ioc d⁻¹ c⁻¹
source
theorem set.inv_mem_Ioc_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
a⁻¹ ∈ set.Ioc c d ↔ a ∈ set.Ico d⁻¹ c⁻¹
source
theorem set.neg_mem_Ioc_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a ∈ set.Ioc c d ↔ a ∈ set.Ico (-d) (-c)
source
theorem set.inv_mem_Ioo_iff {α : Type u_1} [ordered_comm_group α] {a c d : α} :
a⁻¹ ∈ set.Ioo c d ↔ a ∈ set.Ioo d⁻¹ c⁻¹
source
theorem set.neg_mem_Ioo_iff {α : Type u_1} [ordered_add_comm_group α] {a c d : α} :
-a ∈ set.Ioo c d ↔ a ∈ set.Ioo (-d) (-c)

add_mem_Ixx_iff_left

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

add_mem_Ixx_iff_right

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

sub_mem_Ixx_iff_left

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

sub_mem_Ixx_iff_right

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

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

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

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

Equations
source
def order_iso.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
↥(set.Ici ⊥) ≃o α

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

Equations