data.set.intervals.basic

set.Icc_diff_Ico_same

set.Icc_diff_Ioc_same

set.Icc_diff_Ioo_same

set.Icc_diff_both

set.Icc_diff_left

set.Icc_diff_right

set.Icc_eq_empty

set.Icc_eq_empty_iff

set.Icc_inter_Icc

set.Icc_inter_Icc_eq_singleton

set.Icc_subset_Icc

set.Icc_subset_Icc_iff

set.Icc_subset_Icc_left

set.Icc_subset_Icc_right

set.Icc_subset_Icc_union_Icc

set.Icc_subset_Icc_union_Ioc

set.Icc_subset_Ici_iff

set.Icc_subset_Ici_self

set.Icc_subset_Ico_iff

set.Icc_subset_Ico_right

set.Icc_subset_Ico_union_Icc

set.Icc_subset_Iic_iff

set.Icc_subset_Iic_self

set.Icc_subset_Iio_iff

set.Icc_subset_Ioc_iff

set.Icc_subset_Ioi_iff

set.Icc_subset_Ioo

set.Icc_subset_Ioo_iff

set.Icc_union_Icc_eq_Icc

set.Icc_union_Ici_eq_Ici

set.Icc_union_Ico_eq_Ico

set.Icc_union_Ioc_eq_Icc

set.Icc_union_Ioi_eq_Ici

set.Icc_union_Ioo_eq_Ico

set.Ici_diff_Ici

set.Ici_diff_Ioi

set.Ici_diff_Ioi_same

set.Ici_diff_left

set.Ici_inter_Ici

set.Ici_inter_Iic

set.Ici_inter_Iio

set.Ici_subset_Icc_union_Ici

set.Ici_subset_Icc_union_Ioi

set.Ici_subset_Ici

set.Ici_subset_Ico_union_Ici

set.Ici_subset_Ioi

set.Ico_diff_Iio

set.Ico_diff_Ioo_same

set.Ico_diff_left

set.Ico_eq_Ico_iff

set.Ico_eq_empty

set.Ico_eq_empty_iff

set.Ico_inter_Ico

set.Ico_inter_Iio

set.Ico_subset_Icc_self

set.Ico_subset_Icc_union_Ico

set.Ico_subset_Icc_union_Ioo

set.Ico_subset_Ico

set.Ico_subset_Ico_iff

set.Ico_subset_Ico_left

set.Ico_subset_Ico_right

set.Ico_subset_Ico_union_Ico

set.Ico_subset_Iio_self

set.Ico_subset_Ioo_left

set.Ico_union_Icc_eq_Icc

set.Ico_union_Ici_eq_Ici

set.Ico_union_Ico_eq_Ico

set.Iic_diff_Iic

set.Iic_diff_Iio

set.Iic_diff_Iio_same

set.Iic_diff_right

set.Iic_inter_Iic

set.Iic_subset_Iic

set.Iic_subset_Iic_union_Icc

set.Iic_subset_Iic_union_Ioc

set.Iic_subset_Iio

set.Iic_subset_Iio_union_Icc

set.Iic_union_Icc_eq_Iic

set.Iic_union_Ici

set.Iic_union_Ico_eq_Iio

set.Iic_union_Ioc_eq_Iic

set.Iic_union_Ioi

set.Iic_union_Ioo_eq_Iio

set.Iio_diff_Iic

set.Iio_diff_Iio

set.Iio_inter_Iio

set.Iio_subset_Iic

set.Iio_subset_Iic_iff

set.Iio_subset_Iic_self

set.Iio_subset_Iic_union_Ico

set.Iio_subset_Iic_union_Ioo

set.Iio_subset_Iio

set.Iio_subset_Iio_iff

set.Iio_subset_Iio_union_Ico

set.Iio_union_Icc_eq_Iic

set.Iio_union_Ici

set.Iio_union_Ico_eq_Iio

set.Iio_union_right

set.Ioc_diff_Ioo_same

set.Ioc_diff_right

set.Ioc_eq_empty

set.Ioc_inter_Ioc

set.Ioc_subset_Icc_self

set.Ioc_subset_Ioc

set.Ioc_subset_Ioc_left

set.Ioc_subset_Ioc_right

set.Ioc_subset_Ioc_union_Icc

set.Ioc_subset_Ioc_union_Ioc

set.Ioc_subset_Ioi_self

set.Ioc_subset_Ioo_right

set.Ioc_subset_Ioo_union_Icc

set.Ioc_union_Icc_eq_Ioc

set.Ioc_union_Ici_eq_Ioi

set.Ioc_union_Ico_eq_Ioo

set.Ioc_union_Ioc

set.Ioc_union_Ioc_eq_Ioc

set.Ioc_union_Ioc_left

set.Ioc_union_Ioc_right

set.Ioc_union_Ioc_symm

set.Ioc_union_Ioc_union_Ioc_cycle

set.Ioc_union_Ioi_eq_Ioi

set.Ioc_union_Ioo_eq_Ioo

set.Ioi_diff_Ici

set.Ioi_diff_Ioi

set.Ioi_inter_Iic

set.Ioi_inter_Iio

set.Ioi_inter_Ioi

set.Ioi_subset_Ici

set.Ioi_subset_Ici_iff

set.Ioi_subset_Ici_self

set.Ioi_subset_Ioc_union_Ici

set.Ioi_subset_Ioc_union_Ioi

set.Ioi_subset_Ioi

set.Ioi_subset_Ioi_iff

set.Ioi_subset_Ioo_union_Ici

set.Ioi_union_left

set.Ioo_eq_empty

set.Ioo_eq_empty_iff

set.Ioo_inter_Ioo

set.Ioo_subset_Icc_self

set.Ioo_subset_Ico_self

set.Ioo_subset_Iio_self

set.Ioo_subset_Ioc_self

set.Ioo_subset_Ioc_union_Ico

set.Ioo_subset_Ioc_union_Ioo

set.Ioo_subset_Ioi_self

set.Ioo_subset_Ioo

set.Ioo_subset_Ioo_iff

set.Ioo_subset_Ioo_left

set.Ioo_subset_Ioo_right

set.Ioo_subset_Ioo_union_Ico

set.Ioo_union_Icc_eq_Ioc

set.Ioo_union_Ici_eq_Ioi

set.Ioo_union_Ico_eq_Ioo

set.left_mem_Icc

set.left_mem_Ici

set.left_mem_Ico

set.left_mem_Ioc

set.left_mem_Ioo

set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset

set.mem_Ici_Ioi_of_subset_of_subset

set.mem_Iic_Iio_of_subset_of_subset

set.mem_Ioo_or_eq_endpoints_of_mem_Icc

set.mem_Ioo_or_eq_left_of_mem_Ico

set.mem_Ioo_or_eq_right_of_mem_Ioc

set.nonempty_Icc

set.nonempty_Ici

set.nonempty_Ico

set.nonempty_Ico_sdiff

set.nonempty_Iic

set.nonempty_Iio

set.nonempty_Ioc

set.nonempty_Ioi

set.nonempty_Ioo

set.right_mem_Icc

set.right_mem_Ico

set.right_mem_Iic

set.right_mem_Ioc

set.right_mem_Ioo

Intervals

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

i: infinite
o: open
c: closed

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

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

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

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

α → α → set α

Left-open right-open interval

Equations

set.Ioo a b = {x : α | a < x ∧ x < b}

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

α → α → set α

Left-closed right-open interval

Equations

set.Ico a b = {x : α | a ≤ x ∧ x < b}

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

α → set α

Left-infinite right-open interval

Equations

set.Iio a = {x : α | x < a}

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

α → α → set α

Left-closed right-closed interval

Equations

set.Icc a b = {x : α | a ≤ x ∧ x ≤ b}

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

α → set α

Left-infinite right-closed interval

Equations

set.Iic b = {x : α | x ≤ b}

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

α → α → set α

Left-open right-closed interval

Equations

set.Ioc a b = {x : α | a < x ∧ x ≤ b}

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

α → set α

Left-closed right-infinite interval

Equations

set.Ici a = {x : α | a ≤ x}

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

α → set α

Left-open right-infinite interval

Equations

set.Ioi a = {x : α | a < x}

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

{x : α | a < x ∧ x < b} = set.Ioo a b

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

{x : α | a ≤ x ∧ x < b} = set.Ico a b

theorem set.Iio_def {α : Type u} [preorder α] (a : α) :

{x : α | x < a} = set.Iio a

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

{x : α | a ≤ x ∧ x ≤ b} = set.Icc a b

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

{x : α | x ≤ b} = set.Iic b

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

{x : α | a < x ∧ x ≤ b} = set.Ioc a b

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

{x : α | a ≤ x} = set.Ici a

theorem set.Ioi_def {α : Type u} [preorder α] (a : α) :

{x : α | a < x} = set.Ioi a

@[simp]

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

x ∈ set.Ioo a b ↔ a < x ∧ x < b

@[simp]

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

x ∈ set.Ico a b ↔ a ≤ x ∧ x < b

@[simp]

theorem set.mem_Iio {α : Type u} [preorder α] {b x : α} :

x ∈ set.Iio b ↔ x < b

@[simp]

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

x ∈ set.Icc a b ↔ a ≤ x ∧ x ≤ b

@[simp]

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

x ∈ set.Iic b ↔ x ≤ b

@[simp]

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

x ∈ set.Ioc a b ↔ a < x ∧ x ≤ b

@[simp]

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

x ∈ set.Ici a ↔ a ≤ x

@[simp]

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

x ∈ set.Ioi a ↔ a < x

@[simp]

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

a ∈ set.Ioo a b ↔ false

@[simp]

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

a ∈ set.Ico a b ↔ a < b

@[simp]

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

a ∈ set.Icc a b ↔ a ≤ b

@[simp]

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

a ∈ set.Ioc a b ↔ false

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

a ∈ set.Ici a

@[simp]

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

b ∈ set.Ioo a b ↔ false

@[simp]

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

b ∈ set.Ico a b ↔ false

@[simp]

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

b ∈ set.Icc a b ↔ a ≤ b

@[simp]

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

b ∈ set.Ioc a b ↔ a < b

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

a ∈ set.Iic a

@[simp]

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

set.Ici a = set.Iic a

@[simp]

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

set.Iic a = set.Ici a

@[simp]

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

set.Ioi a = set.Iio a

@[simp]

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

set.Iio a = set.Ioi a

@[simp]

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

set.Icc a b = set.Icc b a

@[simp]

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

set.Ioc a b = set.Ico b a

@[simp]

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

set.Ico a b = set.Ioc b a

@[simp]

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

set.Ioo a b = set.Ioo b a

@[simp]

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

(set.Icc a b).nonempty ↔ a ≤ b

@[simp]

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

(set.Ico a b).nonempty ↔ a < b

@[simp]

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

(set.Ioc a b).nonempty ↔ a < b

@[simp]

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

(set.Ici a).nonempty

@[simp]

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

(set.Iic a).nonempty

@[simp]

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

(set.Ioo a b).nonempty ↔ a < b

@[simp]

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

(set.Ioi a).nonempty

@[simp]

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

(set.Iio a).nonempty

@[simp]

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

b ≤ a → set.Ioo a b = ∅

@[simp]

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

b ≤ a → set.Ico a b = ∅

@[simp]

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

b < a → set.Icc a b = ∅

@[simp]

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

b ≤ a → set.Ioc a b = ∅

@[simp]

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

set.Ioo a a = ∅

@[simp]

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

set.Ico a a = ∅

@[simp]

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

set.Ioc a a = ∅

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

set.Ici a ⊆ set.Ici b ↔ b ≤ a

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

set.Iic a ⊆ set.Iic b ↔ a ≤ b

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

set.Ici a ⊆ set.Ioi b ↔ b < a

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

set.Iic a ⊆ set.Iio b ↔ a < b

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

a₂ ≤ a₁ → b₁ ≤ b₂ → set.Ioo a₁ b₁ ⊆ set.Ioo a₂ b₂

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

a₁ ≤ a₂ → set.Ioo a₂ b ⊆ set.Ioo a₁ b

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

b₁ ≤ b₂ → set.Ioo a b₁ ⊆ set.Ioo a b₂

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

a₂ ≤ a₁ → b₁ ≤ b₂ → set.Ico a₁ b₁ ⊆ set.Ico a₂ b₂

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

a₁ ≤ a₂ → set.Ico a₂ b ⊆ set.Ico a₁ b

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

b₁ ≤ b₂ → set.Ico a b₁ ⊆ set.Ico a b₂

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

a₂ ≤ a₁ → b₁ ≤ b₂ → set.Icc a₁ b₁ ⊆ set.Icc a₂ b₂

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

a₁ ≤ a₂ → set.Icc a₂ b ⊆ set.Icc a₁ b

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

b₁ ≤ b₂ → set.Icc a b₁ ⊆ set.Icc a b₂

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

a₂ < a₁ → b₁ < b₂ → set.Icc a₁ b₁ ⊆ set.Ioo a₂ b₂

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

set.Icc a b ⊆ set.Ici a

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

set.Icc a b ⊆ set.Iic b

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

a₂ ≤ a₁ → b₁ ≤ b₂ → set.Ioc a₁ b₁ ⊆ set.Ioc a₂ b₂

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

a₁ ≤ a₂ → set.Ioc a₂ b ⊆ set.Ioc a₁ b

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

b₁ ≤ b₂ → set.Ioc a b₁ ⊆ set.Ioc a b₂

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

a₁ < a₂ → set.Ico a₂ b ⊆ set.Ioo a₁ b

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

b₁ < b₂ → set.Ioc a b₁ ⊆ set.Ioo a b₂

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

b₁ < b₂ → set.Icc a b₁ ⊆ set.Ico a b₂

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

set.Ioo a b ⊆ set.Ico a b

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

set.Ioo a b ⊆ set.Ioc a b

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

set.Ico a b ⊆ set.Icc a b

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

set.Ioc a b ⊆ set.Icc a b

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

set.Ioo a b ⊆ set.Icc a b

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

set.Ico a b ⊆ set.Iio b

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

set.Ioo a b ⊆ set.Iio b

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

set.Ioc a b ⊆ set.Ioi a

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

set.Ioo a b ⊆ set.Ioi a

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

set.Ioi a ⊆ set.Ici a

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

set.Iio a ⊆ set.Iic a

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Iio b₂ ↔ b₁ < b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Ioi a₂ ↔ a₂ < a₁)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Iic b₂ ↔ b₁ ≤ b₂)

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

a₁ ≤ b₁ → (set.Icc a₁ b₁ ⊆ set.Ici a₂ ↔ a₂ ≤ a₁)

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

a ≤ 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.

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

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.

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

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.

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

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.

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

set.Ici a ∩ set.Iic b = set.Icc a b

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

set.Ici a ∩ set.Iio b = set.Ico a b

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

set.Ioi a ∩ set.Iic b = set.Ioc a b

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

set.Ioi a ∩ set.Iio b = set.Ioo a b

@[simp]

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

set.Icc a a = {a}

@[simp]

theorem set.Icc_diff_left {α : Type u} [partial_order α] {a b : α} :

set.Icc a b \ {a} = set.Ioc a b

@[simp]

theorem set.Icc_diff_right {α : Type u} [partial_order α] {a b : α} :

set.Icc a b \ {b} = set.Ico a b

@[simp]

theorem set.Ico_diff_left {α : Type u} [partial_order α] {a b : α} :

set.Ico a b \ {a} = set.Ioo a b

@[simp]

theorem set.Ioc_diff_right {α : Type u} [partial_order α] {a b : α} :

set.Ioc a b \ {b} = set.Ioo a b

@[simp]

theorem set.Icc_diff_both {α : Type u} [partial_order α] {a b : α} :

set.Icc a b \ {a, b} = set.Ioo a b

@[simp]

theorem set.Ici_diff_left {α : Type u} [partial_order α] {a : α} :

set.Ici a \ {a} = set.Ioi a

@[simp]

theorem set.Iic_diff_right {α : Type u} [partial_order α] {a : α} :

set.Iic a \ {a} = set.Iio a

@[simp]

theorem set.Ico_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :

a < b → set.Ico a b \ set.Ioo a b = {a}

@[simp]

theorem set.Ioc_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :

a < b → set.Ioc a b \ set.Ioo a b = {b}

@[simp]

theorem set.Icc_diff_Ico_same {α : Type u} [partial_order α] {a b : α} :

a ≤ b → set.Icc a b \ set.Ico a b = {b}

@[simp]

theorem set.Icc_diff_Ioc_same {α : Type u} [partial_order α] {a b : α} :

a ≤ b → set.Icc a b \ set.Ioc a b = {a}

@[simp]

theorem set.Icc_diff_Ioo_same {α : Type u} [partial_order α] {a b : α} :

a ≤ b → set.Icc a b \ set.Ioo a b = {a, b}

@[simp]

theorem set.Ici_diff_Ioi_same {α : Type u} [partial_order α] {a : α} :

set.Ici a \ set.Ioi a = {a}

@[simp]

theorem set.Iic_diff_Iio_same {α : Type u} [partial_order α] {a : α} :

set.Iic a \ set.Iio a = {a}

@[simp]

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

set.Ioi a ∪ {a} = set.Ici a

@[simp]

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

set.Iio a ∪ {a} = set.Iic a

theorem set.mem_Ici_Ioi_of_subset_of_subset {α : Type u} [partial_order α] {a : α} {s : set α} :

set.Ioi a ⊆ s → s ⊆ set.Ici a → s ∈ {set.Ici a, set.Ioi a}

theorem set.mem_Iic_Iio_of_subset_of_subset {α : Type u} [partial_order α] {a : α} {s : set α} :

set.Iio a ⊆ s → s ⊆ set.Iic a → s ∈ {set.Iic a, set.Iio a}

theorem set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u} [partial_order α] {a b : α} {s : set α} :

set.Ioo a b ⊆ s → s ⊆ set.Icc a b → s ∈ {set.Icc a b, set.Ico a b, set.Ioc a b, set.Ioo a b}

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

x ∈ set.Icc a b → x = a ∨ x = b ∨ x ∈ set.Ioo a b

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

x ∈ set.Ico a b → x = a ∨ x ∈ set.Ioo a b

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

x ∈ set.Ioc a b → x = b ∨ x ∈ set.Ioo a b

@[simp]

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

(set.Iic a)ᶜ = set.Ioi a

@[simp]

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

(set.Ici a)ᶜ = set.Iio a

@[simp]

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

(set.Iio a)ᶜ = set.Ici a

@[simp]

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

(set.Ioi a)ᶜ = set.Iic a

@[simp]

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

set.Ici a \ set.Ici b = set.Ico a b

@[simp]

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

set.Ici a \ set.Ioi b = set.Icc a b

@[simp]

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

set.Ioi a \ set.Ioi b = set.Ioc a b

@[simp]

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

set.Ioi a \ set.Ici b = set.Ioo a b

@[simp]

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

set.Iic b \ set.Iic a = set.Ioc a b

@[simp]

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

set.Iio b \ set.Iic a = set.Ioo a b

@[simp]

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

set.Iic b \ set.Iio a = set.Icc a b

@[simp]

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

set.Iio b \ set.Iio a = set.Ico a b

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

set.Ioo a b = ∅ ↔ b ≤ a

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

set.Ico a b = ∅ ↔ b ≤ a

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

set.Icc a b = ∅ ↔ b < a

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

a₁ < b₁ → (set.Ico a₁ b₁ ⊆ set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)

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

a₁ < b₁ → (set.Ioo a₁ b₁ ⊆ set.Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)

theorem set.Ico_eq_Ico_iff {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :

a₁ < b₁ ∨ a₂ < b₂ → (set.Ico a₁ b₁ = set.Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)

@[simp]

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

set.Ioi b ⊆ set.Ioi a ↔ a ≤ b

@[simp]

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

set.Ioi b ⊆ set.Ici a ↔ a ≤ b

@[simp]

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

set.Iio a ⊆ set.Iio b ↔ a ≤ b

@[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

@[simp]

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

set.Iic a ∪ set.Ici a = set.univ

@[simp]

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

set.Iio a ∪ set.Ici a = set.univ

@[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

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

set.Ioi a ⊆ set.Ioo a b ∪ set.Ici b

@[simp]

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

a < b → set.Ioo a b ∪ set.Ici b = set.Ioi a

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

set.Ici a ⊆ set.Ico a b ∪ set.Ici b

@[simp]

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

a ≤ b → set.Ico a b ∪ set.Ici b = set.Ici a

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

set.Ioi a ⊆ set.Ioc a b ∪ set.Ioi b

@[simp]

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

a ≤ b → set.Ioc a b ∪ set.Ioi b = set.Ioi a

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

set.Ici a ⊆ set.Icc a b ∪ set.Ioi b

@[simp]

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

a ≤ b → set.Icc a b ∪ set.Ioi b = set.Ici a

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

set.Ioi a ⊆ set.Ioc a b ∪ set.Ici b

@[simp]

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

a < b → set.Ioc a b ∪ set.Ici b = set.Ioi a

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

set.Ici a ⊆ set.Icc a b ∪ set.Ici b

@[simp]

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

a ≤ b → set.Icc a b ∪ set.Ici b = set.Ici a

An infinite and a finite interval

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

set.Iic b ⊆ set.Iio a ∪ set.Icc a b

@[simp]

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

a ≤ b → set.Iio a ∪ set.Icc a b = set.Iic b

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

set.Iio b ⊆ set.Iio a ∪ set.Ico a b

@[simp]

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

a ≤ b → set.Iio a ∪ set.Ico a b = set.Iio b

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

set.Iic b ⊆ set.Iic a ∪ set.Ioc a b

@[simp]

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

a ≤ b → set.Iic a ∪ set.Ioc a b = set.Iic b

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

set.Iio b ⊆ set.Iic a ∪ set.Ioo a b

@[simp]

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

a < b → set.Iic a ∪ set.Ioo a b = set.Iio b

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

set.Iic b ⊆ set.Iic a ∪ set.Icc a b

@[simp]

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

a ≤ b → set.Iic a ∪ set.Icc a b = set.Iic b

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

set.Iio b ⊆ set.Iic a ∪ set.Ico a b

@[simp]

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

a < b → set.Iic a ∪ set.Ico a b = set.Iio b

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

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

set.Ioo a c ⊆ set.Ioo a b ∪ set.Ico b c

@[simp]

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

a < b → b ≤ c → set.Ioo a b ∪ set.Ico b c = set.Ioo a c

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

set.Ico a c ⊆ set.Ico a b ∪ set.Ico b c

@[simp]

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

a ≤ b → b ≤ c → set.Ico a b ∪ set.Ico b c = set.Ico a c

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

set.Icc a c ⊆ set.Ico a b ∪ set.Icc b c

@[simp]

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

a ≤ b → b ≤ c → set.Ico a b ∪ set.Icc b c = set.Icc a c

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

set.Ioc a c ⊆ set.Ioo a b ∪ set.Icc b c

@[simp]

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

a < b → b ≤ c → set.Ioo a b ∪ set.Icc b c = set.Ioc a c

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

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

set.Ioo a c ⊆ set.Ioc a b ∪ set.Ioo b c

@[simp]

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

a ≤ b → b < c → set.Ioc a b ∪ set.Ioo b c = set.Ioo a c

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

set.Ico a c ⊆ set.Icc a b ∪ set.Ioo b c

@[simp]

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

a ≤ b → b < c → set.Icc a b ∪ set.Ioo b c = set.Ico a c

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

set.Icc a c ⊆ set.Icc a b ∪ set.Ioc b c

@[simp]

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

a ≤ b → b ≤ c → set.Icc a b ∪ set.Ioc b c = set.Icc a c

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

set.Ioc a c ⊆ set.Ioc a b ∪ set.Ioc b c

@[simp]

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

a ≤ b → b ≤ c → set.Ioc a b ∪ set.Ioc b c = set.Ioc a c

Two finite intervals with a common point

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

set.Ioo a c ⊆ set.Ioc a b ∪ set.Ico b c

@[simp]

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

a < b → b < c → set.Ioc a b ∪ set.Ico b c = set.Ioo a c

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

set.Ico a c ⊆ set.Icc a b ∪ set.Ico b c

@[simp]

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

a ≤ b → b < c → set.Icc a b ∪ set.Ico b c = set.Ico a c

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

set.Icc a c ⊆ set.Icc a b ∪ set.Icc b c

@[simp]

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

a ≤ b → b ≤ c → set.Icc a b ∪ set.Icc b c = set.Icc a c

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

set.Ioc a c ⊆ set.Ioc a b ∪ set.Icc b c

@[simp]

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

a < b → b ≤ c → set.Ioc a b ∪ set.Icc b c = set.Ioc a c

@[simp]

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

set.Iic a ∩ set.Iic b = set.Iic (a ⊓ b)

@[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)

@[simp]

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

set.Ici a ∩ set.Ici b = set.Ici (a ⊔ b)

@[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)

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

set.Icc a₁ b₁ ∩ set.Icc a₂ b₂ = set.Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

@[simp]

theorem set.Icc_inter_Icc_eq_singleton {α : Type u} [lattice α] {a b c : α} :

a ≤ b → b ≤ c → set.Icc a b ∩ set.Icc b c = {b}

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

set.Ico a₁ b₁ ∩ set.Ico a₂ b₂ = set.Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)

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

set.Ioc a₁ b₁ ∩ set.Ioc a₂ b₂ = set.Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

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

set.Ioo a₁ b₁ ∩ set.Ioo a₂ b₂ = set.Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)

@[simp]

theorem set.Ico_diff_Iio {α : Type u} [decidable_linear_order α] {a b c : α} :

set.Ico a b \ set.Iio c = set.Ico (max a c) b

@[simp]

theorem set.Ico_inter_Iio {α : Type u} [decidable_linear_order α] {a b c : α} :

set.Ico a b ∩ set.Iio c = set.Ico a (min b c)

theorem set.Ioc_union_Ioc {α : Type u} [decidable_linear_order α] {a b c d : α} :

min a b ≤ max c d → min c d ≤ max a b → set.Ioc a b ∪ set.Ioc c d = set.Ioc (min a c) (max b d)

@[simp]

theorem set.Ioc_union_Ioc_right {α : Type u} [decidable_linear_order α] {a b c : α} :

set.Ioc a b ∪ set.Ioc a c = set.Ioc a (max b c)

@[simp]

theorem set.Ioc_union_Ioc_left {α : Type u} [decidable_linear_order α] {a b c : α} :

set.Ioc a c ∪ set.Ioc b c = set.Ioc (min a b) c

@[simp]

theorem set.Ioc_union_Ioc_symm {α : Type u} [decidable_linear_order α] {a b : α} :

set.Ioc a b ∪ set.Ioc b a = set.Ioc (min a b) (max a b)

@[simp]

theorem set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u} [decidable_linear_order α] {a b c : α} :

set.Ioc a b ∪ set.Ioc b c ∪ set.Ioc c a = set.Ioc (min a (min b c)) (max a (max b c))

theorem set.nonempty_Ico_sdiff {α : Type u} [decidable_linear_ordered_add_comm_group α] {x dx y dy : α} :

dy < dx → 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

General documentation

Additional documentation

mathlib overview

well founded recursion

documentation style guide

naming conventions

Library

algebra

big_operators

basic

intervals

order

pi

ring

category

Algebra

basic

limits

CommRing

adjunctions

basic

colimits

limits

Group

Z_Module_equivalence

abelian

adjunctions

basic

biproducts

colimits

images

limits

preadditive

zero

Module

abelian

basic

kernels

limits

monoidal

Mon

basic

colimits

limits

continued_fractions

computation

approximations

basic

correctness_terminating

translations

basic

continuants_recurrence

convergents_equiv

terminated_stable

translations

group

basic

commute

conj

defs

hom

inj_surj

pi

prod

semiconj

to_additive

type_tags

ulift

units

units_hom

with_one

homology

chain_complex

exact

homology

image_to_kernel_map

module

basic

ordered

pi

prod

submodule

ulift

polynomial

big_operators

ring

basic

pi

prod

ulift

add_torsor

archimedean

associated

char_p

char_zero

classical_lie_algebras

direct_limit

direct_sum

divisibility

euclidean_domain

field

field_power

floor

free

free_monoid

gcd_monoid

geom_sum

group_action_hom

group_power

group_ring_action

group_with_zero

group_with_zero_power

invertible

iterate_hom

lie_algebra

linear_ordered_comm_group_with_zero

linear_recurrence

midpoint

opposites

order

order_functions

ordered_field

ordered_group

ordered_ring

pointwise

punit_instances

quadratic_discriminant

algebraic_geometry

presheafed_space

prime_spectrum

stalks

analysis

ODE

gronwall

analytic

basic

composition

calculus

darboux

deriv

extend_deriv

fderiv

implicit

inverse

iterated_deriv

lhopital

local_extr

mean_value

specific_functions

tangent_cone

times_cont_diff

complex

basic

polynomial

convex

basic

caratheodory

cone

extrema

specific_functions

topology

normed_space

add_torsor

banach

basic

bounded_linear_maps

complemented

dual

enorm

extend

finite_dimension

hahn_banach

indicator_function

mazur_ulam

multilinear

operator_norm

point_reflection

real_inner_product

riesz_lemma

units

special_functions

arsinh

exp_log

pow

trigonometric

asymptotics

hofer

mean_inequalities

specific_limits

category_theory

abelian

diagram_lemmas

four

basic

exact

non_preadditive

pseudoelements

adjunction

basic

fully_faithful

limits

opposites

category

Cat

Groupoid

Kleisli

Rel

default

closed

cartesian

monoidal

concrete_category

basic

bundled

bundled_hom

reflects_isomorphisms

unbundled_hom

limits

preserves

basic

shapes

shapes

constructions

over

connected

default

products

binary_products

equalizers

limits_of_products_and_equalizers

preserve_binary_products

pullbacks

binary_products

biproducts

concrete_category

equalizers

finite_limits

finite_products

images

kernels

products

pullbacks

regular_mono

strong_epi

terminal

types

wide_pullbacks

zero

concrete_category

cones

connected

creates

fubini

functor_category

lattice

limits

opposites

over

pi

punit

types

monad

adjunction

algebra

basic

bundled

equiv_mon

limits

types

monoidal

internal

functor_category

types

End

braided

category

functor

functor_category

functorial

internal

of_has_finite_products

types

unitors

pi

basic

preadditive

biproducts

default

schur

products

associator

basic

bifunctor

sums

associator

basic

action

arrow

comma

conj

connected

const

core

currying

differential_object

discrete_category

elements

endomorphism

epi_mono

eq_to_hom

equivalence

full_subcategory

fully_faithful

functor

functor_category

functorial

graded_object

groupoid

hom_functor

isomorphism

isomorphism_classes

natural_isomorphism

natural_transformation

opposites

over

pempty

punit

quotient

reflects_isomorphisms

shift

simple

single_obj

sparse

types

whiskering

yoneda

combinatorics

composition

simple_graph

computability

halting

partrec

partrec_code

primrec

reduce

tm_to_partrec

turing_machine

control

bitraversable

basic

instances

lemmas

equiv_functor

instances

functor

multivariate

monad

basic

cont

writer

traversable

basic

derive

equiv

instances

lemmas

applicative

basic

bifunctor

equiv_functor

fold

functor

uliftable

core

data

buffer

parser

bitvec

buffer

dlist

lazy_list

stream

vector

init

algebra

classes

functions

order

control

alternative

applicative

combinators

except

functor

id

lawful

lift

monad

monad_fail

option

reader

state

data

array

basic

slice

bool

basic

lemmas

char

basic

classes

lemmas

fin

basic

ops

int

basic

bitwise

comp_lemmas

order

list

basic

instances

lemmas

qsort

nat

basic

bitwise

div

gcd

lemmas

option

basic

instances

ordering

basic

lemmas

rbmap

basic

rbtree

basic

default

sigma

basic

lex

string

basic

ops

subtype

basic

instances

sum

basic

unsigned

basic

ops

prod

punit

quot

repr

set

setoid

to_string

meta

converter

conv

interactive

lean

parser

smt

congruence_closure

ematch

interactive

rsimp

smt_tactic

widget

basic

html_cmd

interactive_expr

replace_save_info

tactic_component

ac_tactics

async_tactic

attribute

backward

case_tag

comp_value_tactics

congr_lemma

congr_tactic

constructor_tactic

contradiction_tactic

declaration

derive

environment

exceptional

expr

expr_address

float

format

fun_info

has_reflect

hole_command

injection_tactic

interaction_monad

interactive

interactive_base

level

local_context

match_tactic

mk_dec_eq_instance

mk_has_reflect_instance

mk_has_sizeof_instance

mk_inhabited_instance

module_info

name

occurrences

options

pexpr

rb_map

rec_util

ref

relation_tactics

rewrite_tactic

set_get_option_tactics

simp_tactic

tactic

tagged_format

task

type_context

vm

well_founded_tactics

cc_lemmas

classical

coe

core

default

function

funext

ite_simp

logic

propext

util

version

wf

system

io

io_interface

random

data

analysis

filter

topology

array

lemmas

bitvec

basic

buffer

basic

complex

basic

exponential

module

dlist

basic

instances

equiv

encodable

basic

lattice

basic

denumerable

fin

functor

list

local_equiv

mul_add

nat

ring

transfer_instance

finset

basic

fold

intervals

lattice

nat_antidiagonal

order

pi

powerset

sort

finsupp

basic

lattice

pointwise

fintype

basic

card

intervals

sort

fp

basic

int

basic

cast

char_zero

gcd

modeq

parity

range

sqrt

list

alist

bag_inter

basic

chain

defs

erase_dup

forall2

func

indexes

intervals

min_max

nat_antidiagonal

nodup

of_fn

pairwise

palindrome

perm

range

rotate

sections

sigma

sort

tfae

zip

matrix

basic

notation

pequiv

multiset

antidiagonal

basic

erase_dup

finset_ops

fold

functor

intervals

lattice

nat_antidiagonal

nodup

pi

powerset

range

sections

sort

nat

basic

cast

choose

digits

dist

enat

fib

gcd

modeq

multiplicity

pairing

parity

prime

sqrt

totient

num

basic

bitwise

lemmas

prime

option

basic

defs

padics

hensel

padic_integers

padic_norm

padic_numbers

pfunctor

multivariate

M

W

basic

univariate

M

basic

pnat

basic

factors

intervals

xgcd

polynomial

degree

basic

algebra_map

basic

coeff

degree

derivative

div

eval

field_division

identities

induction

integral_normalization

monic

monomial

ring_division

qpf

multivariate

constructions

cofix

comp

const

fix

prj

quot

sigma

basic

univariate

basic

rat

basic

cast

denumerable

floor

meta_defs

order

sqrt

real

basic

cardinality

cau_seq

cau_seq_completion

conjugate_exponents

ennreal

ereal

golden_ratio

hyperreal

irrational

nnreal

pi

seq

computation

parallel

seq

wseq

set

intervals

basic

disjoint

image_preimage

ord_connected

unordered_interval

basic

countable

disjointed

enumerate

finite

function

lattice

setoid

basic

partition

sigma

basic

stream

basic

string

basic

defs

zmod

basic

zsqrtd

basic

gaussian_int

W

bool

char

dfinsupp

erased

fin

fin2

fin_enum

finmap

hash_map

holor

indicator_function

lazy_list2

mllist

monoid_algebra

mv_polynomial

opposite

pequiv

pfun

prod

quot

rel

semiquot

subtype

sum

support

sym

sym2

tree

typevec

ulift

vector2

deprecated

group

ring

subgroup

submonoid

dynamics

circle

rotation_number

translation_number

fixed_points

basic

topology

periodic_pts

field_theory

algebraic_closure

chevalley_warning

finite

fixed

minimal_polynomial

mv_polynomial

normal

perfect_closure

separable

splitting_field

subfield

tower

geometry

algebra

lie_group

euclidean

basic

circumcenter

monge_point

triangle

manifold

basic_smooth_bundle

charted_space

local_invariant_properties

mfderiv

real_instances

smooth_manifold_with_corners

times_cont_mdiff

group_theory

perm

cycles

sign

submonoid

basic

membership

operations

abelianization

congruence

coset

eckmann_hilton

free_abelian_group

free_group

group_action

monoid_localization

order_of_element

presented_group

quotient_group

semidirect_product

subgroup

sylow

linear_algebra

affine_space

basic

combination

finite_dimensional

independent

char_poly

coeff

direct_sum

finsupp

tensor_product

adic_completion

basic

basis

bilinear_form

char_poly

contraction

determinant

dimension

direct_sum_module

dual

finite_dimensional

finsupp

finsupp_vector_space

invariant_basis_number

lagrange

linear_action

linear_pmap

matrix

multilinear

nonsingular_inverse

projection

quadratic_form

sesquilinear_form

smodeq

special_linear_group

tensor_algebra

tensor_product

logic

function

basic

conjugate

iterate

basic

embedding

nontrivial

relation

relator

unique

measure_theory

category

Meas

ae_eq_fun

bochner_integration

borel_space

content

decomposition

giry_monad

group

haar_measure

integration

interval_integral

l1_space

lebesgue_measure

measurable_space

measure_space

outer_measure

probability_mass_function

set_integral

simple_func_dense

meta

coinductive_predicates

expr

expr_lens

rb_map

uchange

number_theory

basic

bernoulli

dioph

lucas_lehmer

pell

primorial

pythagorean_triples

quadratic_reciprocity

sum_four_squares

sum_two_squares

order

category

LinearOrder

NonemptyFinLinOrd

PartialOrder

Preorder

filter

at_top_bot

bases

basic

cofinite

countable_Inter

extr

filter_product

germ

indicator_function

interval

lift

partial

pointwise

ultrafilter

basic

boolean_algebra

bounded_lattice

bounds

complete_boolean_algebra

complete_lattice

conditionally_complete_lattice

copy

directed

fixed_points

galois_connection

ideal

iterate

lattice

lexicographic

liminf_limsup

ord_continuous

order_iso_nat

pilex

rel_classes

rel_iso

semiconj_Sup

zorn

representation_theory

maschke

ring_theory

ideal

basic

operations

over

polynomial

basic

homogeneous

rational_root

valuation

basic

adjoin

adjoin_root

algebra

algebra_operations

algebra_tower

algebraic

coprime

derivation

discrete_valuation_ring

eisenstein_criterion

euclidean_domain

fintype

fractional_ideal

free_comm_ring

free_ring

integral_closure

integral_domain

jacobson

jacobson_ideal

localization

maps

matrix_algebra

multiplicity

noetherian

polynomial_algebra

power_series

prime

principal_ideal_domain

subring

subsemiring

tensor_product

unique_factorization_domain

set_theory

game

domineering

impartial

nim

short

state

winner

cardinal

cardinal_ordinal

cofinality

game

lists

ordinal

ordinal_arithmetic

ordinal_notation

pgame

schroeder_bernstein

surreal

zfc

system

random

basic

tactic

converter

apply_congr

binders

interactive

old_conv

linarith

datatypes

elimination

frontend

lemmas

parsing

preprocessing

verification

lint

basic

default

frontend

misc

simp

type_classes

monotonicity

basic

interactive

lemmas

nth_rewrite

basic

congr

default

omega

int

dnf

form

main

preterm

nat

dnf

form

main

neg_elim

preterm

sub_elim

clause

coeffs

eq_elim

find_ees

find_scalars

lin_comb

main

misc

prove_unsats

term

rewrite_all

basic

abel

algebra

alias

apply

apply_fun

auto_cases

binder_matching

cache

cancel_denoms

chain

choose

clear

core

dec_trivial

delta_instance

derive_fintype

derive_inhabited

doc_commands

elide

equiv_rw

explode

ext

fin_cases

find

find_unused

finish

fix_reflect_string

generalize_proofs

generalizes

group

hint

interactive

interactive_expr

interval_cases

lift

local_cache

localized

mk_iff_of_inductive_prop

noncomm_ring

norm_cast

norm_num

obviously

pi_instances

protected

push_neg

rcases

reassoc_axiom

rename_var

replacer

restate_axiom

rewrite

ring

ring2

ring_exp

scc

show_term

simp_command

simp_result

simp_rw

simpa

simps

slice

solve_by_elim

split_ifs

squeeze

subtype_instance

suggest

tauto

tfae

tidy

transfer

transform_decl

transport

trunc_cases

unfold_cases

where

with_local_reducibility

wlog

zify

topology

algebra

affine

continuous_functions

group

group_completion

infinite_sum

module

monoid

multilinear

open_subgroup

ordered

polynomial

ring

uniform_group

uniform_ring

category

Top

adjunctions

basic

epi_mono

limits

open_nhds

opens

TopCommRing

UniformSpace

instances

complex

ennreal

nnreal

real

real_vector_space

metric_space

antilipschitz

baire

basic

cau_seq_filter

closeds

completion

contracting

emetric_space

gluing

gromov_hausdorff

gromov_hausdorff_realized

hausdorff_distance

isometry

lipschitz

pi_Lp

premetric_space

sheaves

presheaf

presheaf_of_functions

sheaf

sheaf_of_functions

stalks

uniform_space

absolute_value

abstract_completion

basic

cauchy

compact_separated

compare_reals

complete_separated

completion

pi

separation

uniform_convergence

uniform_embedding

bases

basic

bounded_continuous_function

compact_open

compacts

constructions

continuous_map

continuous_on

dense_embedding

extend_from_subset

homeomorph

list

local_extr

local_homeomorph

maps

opens

order

path_connected

separation

sequences

stone_cech

subset_properties

tactic

topological_fiber_bundle