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 interval (a, b]. The definitions can be found in Order/Interval/Set/Defs.

This file contains 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 LinearOrder or DenselyOrdered).

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

instance Set.decidableMemIoo {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x ∧ x < b)] : Decidable (x ∈ Set.Ioo a b)

Equations

• Set.decidableMemIoo = inst

instance Set.decidableMemIco {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x ∧ x < b)] : Decidable (x ∈ Set.Ico a b)

Equations

• Set.decidableMemIco = inst

instance Set.decidableMemIio {α : Type u_1} [Preorder α] {b x : α} [Decidable (x < b)] : Decidable (x ∈ Set.Iio b)

Equations

• Set.decidableMemIio = inst

instance Set.decidableMemIcc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x ∧ x ≤ b)] : Decidable (x ∈ Set.Icc a b)

Equations

• Set.decidableMemIcc = inst

instance Set.decidableMemIic {α : Type u_1} [Preorder α] {b x : α} [Decidable (x ≤ b)] : Decidable (x ∈ Set.Iic b)

Equations

• Set.decidableMemIic = inst

instance Set.decidableMemIoc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x ∧ x ≤ b)] : Decidable (x ∈ Set.Ioc a b)

Equations

• Set.decidableMemIoc = inst

instance Set.decidableMemIci {α : Type u_1} [Preorder α] {a x : α} [Decidable (a ≤ x)] : Decidable (x ∈ Set.Ici a)

Equations

• Set.decidableMemIci = inst

instance Set.decidableMemIoi {α : Type u_1} [Preorder α] {a x : α} [Decidable (a < x)] : Decidable (x ∈ Set.Ioi a)

Equations

• Set.decidableMemIoi = inst

theorem Set.left_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} : a ∈ Set.Ioo a b ↔ False

theorem Set.left_mem_Ico {α : Type u_1} [Preorder α] {a b : α} : a ∈ Set.Ico a b ↔ a < b

theorem Set.left_mem_Icc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Set.Icc a b ↔ a ≤ b

theorem Set.left_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} : a ∈ Set.Ioc a b ↔ False

theorem Set.left_mem_Ici {α : Type u_1} [Preorder α] {a : α} : a ∈ Set.Ici a

theorem Set.right_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} : b ∈ Set.Ioo a b ↔ False

theorem Set.right_mem_Ico {α : Type u_1} [Preorder α] {a b : α} : b ∈ Set.Ico a b ↔ False

theorem Set.right_mem_Icc {α : Type u_1} [Preorder α] {a b : α} : b ∈ Set.Icc a b ↔ a ≤ b

theorem Set.right_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} : b ∈ Set.Ioc a b ↔ a < b

theorem Set.right_mem_Iic {α : Type u_1} [Preorder α] {a : α} : a ∈ Set.Iic a

@[simp]

theorem Set.dual_Ici {α : Type u_1} [Preorder α] {a : α} : Set.Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iic a

@[simp]

theorem Set.dual_Iic {α : Type u_1} [Preorder α] {a : α} : Set.Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ici a

@[simp]

theorem Set.dual_Ioi {α : Type u_1} [Preorder α] {a : α} : Set.Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iio a

@[simp]

theorem Set.dual_Iio {α : Type u_1} [Preorder α] {a : α} : Set.Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Ioi a

@[simp]

theorem Set.dual_Icc {α : Type u_1} [Preorder α] {a b : α} : Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a

@[simp]

theorem Set.dual_Ioc {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ico b a

@[simp]

theorem Set.dual_Ico {α : Type u_1} [Preorder α] {a b : α} : Set.Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioc b a

@[simp]

theorem Set.dual_Ioo {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioo b a

@[simp]

theorem Set.nonempty_Icc {α : Type u_1} [Preorder α] {a b : α} : (Set.Icc a b).Nonempty ↔ a ≤ b

@[simp]

theorem Set.nonempty_Ico {α : Type u_1} [Preorder α] {a b : α} : (Set.Ico a b).Nonempty ↔ a < b

@[simp]

theorem Set.nonempty_Ioc {α : Type u_1} [Preorder α] {a b : α} : (Set.Ioc a b).Nonempty ↔ a < b

@[simp]

theorem Set.nonempty_Ici {α : Type u_1} [Preorder α] {a : α} : (Set.Ici a).Nonempty

@[simp]

theorem Set.nonempty_Iic {α : Type u_1} [Preorder α] {a : α} : (Set.Iic a).Nonempty

@[simp]

theorem Set.nonempty_Ioo {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] : (Set.Ioo a b).Nonempty ↔ a < b

@[simp]

theorem Set.nonempty_Ioi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : (Set.Ioi a).Nonempty

@[simp]

theorem Set.nonempty_Iio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] : (Set.Iio a).Nonempty

theorem Set.nonempty_Icc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : Nonempty ↑(Set.Icc a b)

theorem Set.nonempty_Ico_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : Nonempty ↑(Set.Ico a b)

theorem Set.nonempty_Ioc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : Nonempty ↑(Set.Ioc a b)

instance Set.nonempty_Ici_subtype {α : Type u_1} [Preorder α] {a : α} : Nonempty ↑(Set.Ici a)

An interval Ici a is nonempty.

Equations

• ⋯ = ⋯

instance Set.nonempty_Iic_subtype {α : Type u_1} [Preorder α] {a : α} : Nonempty ↑(Set.Iic a)

An interval Iic a is nonempty.

Equations

• ⋯ = ⋯

theorem Set.nonempty_Ioo_subtype {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] (h : a < b) : Nonempty ↑(Set.Ioo a b)

instance Set.nonempty_Ioi_subtype {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : Nonempty ↑(Set.Ioi a)

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

Equations

• ⋯ = ⋯

instance Set.nonempty_Iio_subtype {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] : Nonempty ↑(Set.Iio a)

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

Equations

• ⋯ = ⋯

instance Set.instNoMinOrderElemIio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] : NoMinOrder ↑(Set.Iio a)

Equations

• ⋯ = ⋯

instance Set.instNoMinOrderElemIic {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] : NoMinOrder ↑(Set.Iic a)

Equations

• ⋯ = ⋯

instance Set.instNoMaxOrderElemIoi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : NoMaxOrder ↑(Set.Ioi a)

Equations

• ⋯ = ⋯

instance Set.instNoMaxOrderElemIci {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] : NoMaxOrder ↑(Set.Ici a)

Equations

• ⋯ = ⋯

@[simp]

theorem Set.Icc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a ≤ b) : Set.Icc a b = ∅

@[simp]

theorem Set.Ico_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) : Set.Ico a b = ∅

@[simp]

theorem Set.Ioc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) : Set.Ioc a b = ∅

@[simp]

theorem Set.Ioo_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) : Set.Ioo a b = ∅

@[simp]

theorem Set.Icc_eq_empty_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : Set.Icc a b = ∅

@[simp]

theorem Set.Ico_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : Set.Ico a b = ∅

@[simp]

theorem Set.Ioc_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : Set.Ioc a b = ∅

@[simp]

theorem Set.Ioo_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) : Set.Ioo a b = ∅

theorem Set.Ico_self {α : Type u_1} [Preorder α] (a : α) : Set.Ico a a = ∅

theorem Set.Ioc_self {α : Type u_1} [Preorder α] (a : α) : Set.Ioc a a = ∅

theorem Set.Ioo_self {α : Type u_1} [Preorder α] (a : α) : Set.Ioo a a = ∅

theorem Set.Ici_subset_Ici {α : Type u_1} [Preorder α] {a b : α} : Set.Ici a ⊆ Set.Ici b ↔ b ≤ a

theorem GCongr.Ici_subset_Ici_of_le {α : Type u_1} [Preorder α] {a b : α} : b ≤ a → Set.Ici a ⊆ Set.Ici b

Alias of the reverse direction of Set.Ici_subset_Ici.

theorem Set.Iic_subset_Iic {α : Type u_1} [Preorder α] {a b : α} : Set.Iic a ⊆ Set.Iic b ↔ a ≤ b

theorem GCongr.Iic_subset_Iic_of_le {α : Type u_1} [Preorder α] {a b : α} : a ≤ b → Set.Iic a ⊆ Set.Iic b

Alias of the reverse direction of Set.Iic_subset_Iic.

theorem Set.Ici_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} : Set.Ici a ⊆ Set.Ioi b ↔ b < a

theorem Set.Iic_subset_Iio {α : Type u_1} [Preorder α] {a b : α} : Set.Iic a ⊆ Set.Iio b ↔ a < b

theorem Set.Ioo_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂

theorem Set.Ioo_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Set.Ioo a₂ b ⊆ Set.Ioo a₁ b

theorem Set.Ioo_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) : Set.Ioo a b₁ ⊆ Set.Ioo a b₂

theorem Set.Ico_subset_Ico {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂

theorem Set.Ico_subset_Ico_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Set.Ico a₂ b ⊆ Set.Ico a₁ b

theorem Set.Ico_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) : Set.Ico a b₁ ⊆ Set.Ico a b₂

theorem Set.Icc_subset_Icc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂

theorem Set.Icc_subset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Set.Icc a₂ b ⊆ Set.Icc a₁ b

theorem Set.Icc_subset_Icc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) : Set.Icc a b₁ ⊆ Set.Icc a b₂

theorem Set.Icc_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ < b₂) : Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂

theorem Set.Icc_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} : Set.Icc a b ⊆ Set.Ici a

theorem Set.Icc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} : Set.Icc a b ⊆ Set.Iic b

theorem Set.Ioc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc a b ⊆ Set.Iic b

theorem Set.Ioc_subset_Ioc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) : Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂

theorem Set.Ioc_subset_Ioc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) : Set.Ioc a₂ b ⊆ Set.Ioc a₁ b

theorem Set.Ioc_subset_Ioc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) : Set.Ioc a b₁ ⊆ Set.Ioc a b₂

theorem Set.Ico_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h₁ : a₁ < a₂) : Set.Ico a₂ b ⊆ Set.Ioo a₁ b

theorem Set.Ioc_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) : Set.Ioc a b₁ ⊆ Set.Ioo a b₂

theorem Set.Icc_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h₁ : b₁ < b₂) : Set.Icc a b₁ ⊆ Set.Ico a b₂

theorem Set.Ioo_subset_Ico_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo a b ⊆ Set.Ico a b

theorem Set.Ioo_subset_Ioc_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo a b ⊆ Set.Ioc a b

theorem Set.Ico_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ico a b ⊆ Set.Icc a b

theorem Set.Ioc_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc a b ⊆ Set.Icc a b

theorem Set.Ioo_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo a b ⊆ Set.Icc a b

theorem Set.Ico_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ico a b ⊆ Set.Iio b

theorem Set.Ioo_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo a b ⊆ Set.Iio b

theorem Set.Ioc_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc a b ⊆ Set.Ioi a

theorem Set.Ioo_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo a b ⊆ Set.Ioi a

theorem Set.Ioi_subset_Ici_self {α : Type u_1} [Preorder α] {a : α} : Set.Ioi a ⊆ Set.Ici a

theorem Set.Iio_subset_Iic_self {α : Type u_1} [Preorder α] {a : α} : Set.Iio a ⊆ Set.Iic a

theorem Set.Ico_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} : Set.Ico a b ⊆ Set.Ici a

theorem Set.Ioi_ssubset_Ici_self {α : Type u_1} [Preorder α] {a : α} : Set.Ioi a ⊂ Set.Ici a

theorem Set.Iio_ssubset_Iic_self {α : Type u_1} [Preorder α] {a : α} : Set.Iio a ⊂ Set.Iic a

theorem Set.Icc_subset_Icc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

theorem Set.Icc_subset_Ioo_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

theorem Set.Icc_subset_Ico_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

theorem Set.Icc_subset_Ioc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

theorem Set.Icc_subset_Iio_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Iio b₂ ↔ b₁ < b₂

theorem Set.Icc_subset_Ioi_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Ioi a₂ ↔ a₂ < a₁

theorem Set.Icc_subset_Iic_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Iic b₂ ↔ b₁ ≤ b₂

theorem Set.Icc_subset_Ici_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ ≤ b₁) : Set.Icc a₁ b₁ ⊆ Set.Ici a₂ ↔ a₂ ≤ a₁

theorem Set.Icc_ssubset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

theorem Set.Icc_ssubset_Icc_right {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

theorem Set.Ioi_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : 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_1} [Preorder α] {a b : α} (h : a ≤ b) : Set.Ioi b ⊆ Set.Ici a

If a ≤ b, then (b, +∞) ⊆ [a, +∞). In preorders, this is just an implication. If you need the equivalence in dense linear orders, use Ioi_subset_Ici_iff.

theorem Set.Iio_subset_Iio {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : Set.Iio a ⊆ Set.Iio b

If a ≤ b, then (-∞, a) ⊆ (-∞, b). In preorders, this is just an implication. If you need the equivalence in linear orders, use Iio_subset_Iio_iff.

theorem Set.Iio_subset_Iic {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) : Set.Iio a ⊆ Set.Iic b

If a ≤ b, then (-∞, a) ⊆ (-∞, b]. In preorders, this is just an implication. If you need the equivalence in dense linear orders, use Iio_subset_Iic_iff.

theorem Set.Ici_inter_Iic {α : Type u_1} [Preorder α] {a b : α} : Set.Ici a ∩ Set.Iic b = Set.Icc a b

theorem Set.Ici_inter_Iio {α : Type u_1} [Preorder α] {a b : α} : Set.Ici a ∩ Set.Iio b = Set.Ico a b

theorem Set.Ioi_inter_Iic {α : Type u_1} [Preorder α] {a b : α} : Set.Ioi a ∩ Set.Iic b = Set.Ioc a b

theorem Set.Ioi_inter_Iio {α : Type u_1} [Preorder α] {a b : α} : Set.Ioi a ∩ Set.Iio b = Set.Ioo a b

theorem Set.Iic_inter_Ici {α : Type u_1} [Preorder α] {a b : α} : Set.Iic a ∩ Set.Ici b = Set.Icc b a

theorem Set.Iio_inter_Ici {α : Type u_1} [Preorder α] {a b : α} : Set.Iio a ∩ Set.Ici b = Set.Ico b a

theorem Set.Iic_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} : Set.Iic a ∩ Set.Ioi b = Set.Ioc b a

theorem Set.Iio_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} : Set.Iio a ∩ Set.Ioi b = Set.Ioo b a

theorem Set.mem_Icc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Set.Ioo a b) : x ∈ Set.Icc a b

theorem Set.mem_Ico_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Set.Ioo a b) : x ∈ Set.Ico a b

theorem Set.mem_Ioc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Set.Ioo a b) : x ∈ Set.Ioc a b

theorem Set.mem_Icc_of_Ico {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Set.Ico a b) : x ∈ Set.Icc a b

theorem Set.mem_Icc_of_Ioc {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Set.Ioc a b) : x ∈ Set.Icc a b

theorem Set.mem_Ici_of_Ioi {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Set.Ioi a) : x ∈ Set.Ici a

theorem Set.mem_Iic_of_Iio {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Set.Iio a) : x ∈ Set.Iic a

theorem Set.Icc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} : Set.Icc a b = ∅ ↔ ¬a ≤ b

theorem Set.Ico_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} : Set.Ico a b = ∅ ↔ ¬a < b

theorem Set.Ioc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc a b = ∅ ↔ ¬a < b

theorem Set.Ioo_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] : Set.Ioo a b = ∅ ↔ ¬a < b

theorem IsTop.Iic_eq {α : Type u_1} [Preorder α] {a : α} (h : IsTop a) : Set.Iic a = Set.univ

theorem IsBot.Ici_eq {α : Type u_1} [Preorder α] {a : α} (h : IsBot a) : Set.Ici a = Set.univ

theorem Set.Ioi_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} : Set.Ioi a = ∅ ↔ IsMax a

theorem Set.Iio_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} : Set.Iio a = ∅ ↔ IsMin a

theorem IsMax.Ioi_eq {α : Type u_1} [Preorder α] {a : α} : IsMax a → Set.Ioi a = ∅

Alias of the reverse direction of Set.Ioi_eq_empty_iff.

theorem IsMin.Iio_eq {α : Type u_1} [Preorder α] {a : α} : IsMin a → Set.Iio a = ∅

Alias of the reverse direction of Set.Iio_eq_empty_iff.

theorem Set.Iic_inter_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (h : a ≤ c) : Set.Iic a ∩ Set.Ioc b c = Set.Ioc b a

theorem Set.not_mem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) : c ∉ Set.Icc a b

theorem Set.not_mem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) : c ∉ Set.Icc a b

theorem Set.not_mem_Ico_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) : c ∉ Set.Ico a b

theorem Set.not_mem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) : c ∉ Set.Ioc a b

theorem Set.not_mem_Ioi_self {α : Type u_1} [Preorder α] {a : α} : a ∉ Set.Ioi a

theorem Set.not_mem_Iio_self {α : Type u_1} [Preorder α] {b : α} : b ∉ Set.Iio b

theorem Set.not_mem_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) : c ∉ Set.Ioc a b

theorem Set.not_mem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b ≤ c) : c ∉ Set.Ico a b

theorem Set.not_mem_Ioo_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) : c ∉ Set.Ioo a b

theorem Set.not_mem_Ioo_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b ≤ c) : c ∉ Set.Ioo a b

@[simp]

theorem Set.Icc_self {α : Type u_1} [PartialOrder α] (a : α) : Set.Icc a a = {a}

instance Set.instIccUnique {α : Type u_1} [PartialOrder α] {a : α} : Unique ↑(Set.Icc a a)

Equations

• Set.instIccUnique = { default := ⟨a, ⋯⟩, uniq := ⋯ }

@[simp]

theorem Set.Icc_eq_singleton_iff {α : Type u_1} [PartialOrder α] {a b c : α} : Set.Icc a b = {c} ↔ a = c ∧ b = c

theorem Set.subsingleton_Icc_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (hba : b ≤ a) : (Set.Icc a b).Subsingleton

@[simp]

theorem Set.subsingleton_Icc_iff {α : Type u_3} [LinearOrder α] {a b : α} : (Set.Icc a b).Subsingleton ↔ b ≤ a

@[simp]

theorem Set.Icc_diff_left {α : Type u_1} [PartialOrder α] {a b : α} : Set.Icc a b \ {a} = Set.Ioc a b

@[simp]

theorem Set.Icc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} : Set.Icc a b \ {b} = Set.Ico a b

@[simp]

theorem Set.Ico_diff_left {α : Type u_1} [PartialOrder α] {a b : α} : Set.Ico a b \ {a} = Set.Ioo a b

@[simp]

theorem Set.Ioc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} : Set.Ioc a b \ {b} = Set.Ioo a b

@[simp]

theorem Set.Icc_diff_both {α : Type u_1} [PartialOrder α] {a b : α} : Set.Icc a b \ {a, b} = Set.Ioo a b

@[simp]

theorem Set.Ici_diff_left {α : Type u_1} [PartialOrder α] {a : α} : Set.Ici a \ {a} = Set.Ioi a

@[simp]

theorem Set.Iic_diff_right {α : Type u_1} [PartialOrder α] {a : α} : Set.Iic a \ {a} = Set.Iio a

@[simp]

theorem Set.Ico_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : Set.Ico a b \ Set.Ioo a b = {a}

@[simp]

theorem Set.Ioc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : Set.Ioc a b \ Set.Ioo a b = {b}

@[simp]

theorem Set.Icc_diff_Ico_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Set.Icc a b \ Set.Ico a b = {b}

@[simp]

theorem Set.Icc_diff_Ioc_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Set.Icc a b \ Set.Ioc a b = {a}

@[simp]

theorem Set.Icc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Set.Icc a b \ Set.Ioo a b = {a, b}

@[simp]

theorem Set.Ici_diff_Ioi_same {α : Type u_1} [PartialOrder α] {a : α} : Set.Ici a \ Set.Ioi a = {a}

@[simp]

theorem Set.Iic_diff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} : Set.Iic a \ Set.Iio a = {a}

theorem Set.Ioi_union_left {α : Type u_1} [PartialOrder α] {a : α} : Set.Ioi a ∪ {a} = Set.Ici a

theorem Set.Iio_union_right {α : Type u_1} [PartialOrder α] {a : α} : Set.Iio a ∪ {a} = Set.Iic a

theorem Set.Ioo_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) : Set.Ioo a b ∪ {a} = Set.Ico a b

theorem Set.Ioo_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) : Set.Ioo a b ∪ {b} = Set.Ioc a b

theorem Set.Ioo_union_both {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : Set.Ioo a b ∪ {a, b} = Set.Icc a b

theorem Set.Ioc_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a ≤ b) : Set.Ioc a b ∪ {a} = Set.Icc a b

theorem Set.Ico_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a ≤ b) : Set.Ico a b ∪ {b} = Set.Icc a b

@[simp]

theorem Set.Ico_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : insert b (Set.Ico a b) = Set.Icc a b

@[simp]

theorem Set.Ioc_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) : insert a (Set.Ioc a b) = Set.Icc a b

@[simp]

theorem Set.Ioo_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : insert a (Set.Ioo a b) = Set.Ico a b

@[simp]

theorem Set.Ioo_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) : insert b (Set.Ioo a b) = Set.Ioc a b

@[simp]

theorem Set.Iio_insert {α : Type u_1} [PartialOrder α] {a : α} : insert a (Set.Iio a) = Set.Iic a

@[simp]

theorem Set.Ioi_insert {α : Type u_1} [PartialOrder α] {a : α} : insert a (Set.Ioi a) = Set.Ici a

theorem Set.mem_Ici_Ioi_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Set.Ioi a ⊆ s) (hc : s ⊆ Set.Ici a) : s ∈ {Set.Ici a, Set.Ioi a}

theorem Set.mem_Iic_Iio_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Set.Iio a ⊆ s) (hc : s ⊆ Set.Iic a) : s ∈ {Set.Iic a, Set.Iio a}

theorem Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u_1} [PartialOrder α] {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}

theorem Set.eq_left_or_mem_Ioo_of_mem_Ico {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Set.Ico a b) : x = a ∨ x ∈ Set.Ioo a b

theorem Set.eq_right_or_mem_Ioo_of_mem_Ioc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Set.Ioc a b) : x = b ∨ x ∈ Set.Ioo a b

theorem Set.eq_endpoints_or_mem_Ioo_of_mem_Icc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Set.Icc a b) : x = a ∨ x = b ∨ x ∈ Set.Ioo a b

theorem IsMax.Ici_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMax a) : Set.Ici a = {a}

theorem IsMin.Iic_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMin a) : Set.Iic a = {a}

theorem Set.Ici_injective {α : Type u_1} [PartialOrder α] : Function.Injective Set.Ici

theorem Set.Iic_injective {α : Type u_1} [PartialOrder α] : Function.Injective Set.Iic

theorem Set.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} : Set.Ici a = Set.Ici b ↔ a = b

theorem Set.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} : Set.Iic a = Set.Iic b ↔ a = b

@[simp]

theorem Set.Ici_top {α : Type u_1} [PartialOrder α] [OrderTop α] : Set.Ici ⊤ = {⊤}

@[simp]

theorem Set.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] : Set.Ioi ⊤ = ∅

@[simp]

theorem Set.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] : Set.Iic ⊤ = Set.univ

@[simp]

theorem Set.Icc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} : Set.Icc a ⊤ = Set.Ici a

@[simp]

theorem Set.Ioc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} : Set.Ioc a ⊤ = Set.Ioi a

@[simp]

theorem Set.Iic_bot {α : Type u_1} [PartialOrder α] [OrderBot α] : Set.Iic ⊥ = {⊥}

@[simp]

theorem Set.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] : Set.Iio ⊥ = ∅

@[simp]

theorem Set.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] : Set.Ici ⊥ = Set.univ

@[simp]

theorem Set.Icc_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} : Set.Icc ⊥ a = Set.Iic a

@[simp]

theorem Set.Ico_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} : Set.Ico ⊥ a = Set.Iio a

theorem Set.Icc_bot_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] : Set.Icc ⊥ ⊤ = Set.univ

theorem Set.not_mem_Ici {α : Type u_1} [LinearOrder α] {a c : α} : c ∉ Set.Ici a ↔ c < a

theorem Set.not_mem_Iic {α : Type u_1} [LinearOrder α] {b c : α} : c ∉ Set.Iic b ↔ b < c

theorem Set.not_mem_Ioi {α : Type u_1} [LinearOrder α] {a c : α} : c ∉ Set.Ioi a ↔ c ≤ a

theorem Set.not_mem_Iio {α : Type u_1} [LinearOrder α] {b c : α} : c ∉ Set.Iio b ↔ b ≤ c

@[simp]

theorem Set.compl_Iic {α : Type u_1} [LinearOrder α] {a : α} : (Set.Iic a)ᶜ = Set.Ioi a

@[simp]

theorem Set.compl_Ici {α : Type u_1} [LinearOrder α] {a : α} : (Set.Ici a)ᶜ = Set.Iio a

@[simp]

theorem Set.compl_Iio {α : Type u_1} [LinearOrder α] {a : α} : (Set.Iio a)ᶜ = Set.Ici a

@[simp]

theorem Set.compl_Ioi {α : Type u_1} [LinearOrder α] {a : α} : (Set.Ioi a)ᶜ = Set.Iic a

@[simp]

theorem Set.Ici_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ici a \ Set.Ici b = Set.Ico a b

@[simp]

theorem Set.Ici_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ici a \ Set.Ioi b = Set.Icc a b

@[simp]

theorem Set.Ioi_diff_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a \ Set.Ioi b = Set.Ioc a b

@[simp]

theorem Set.Ioi_diff_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a \ Set.Ici b = Set.Ioo a b

@[simp]

theorem Set.Iic_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iic b \ Set.Iic a = Set.Ioc a b

@[simp]

theorem Set.Iio_diff_Iic {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio b \ Set.Iic a = Set.Ioo a b

@[simp]

theorem Set.Iic_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iic b \ Set.Iio a = Set.Icc a b

@[simp]

theorem Set.Iio_diff_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio b \ Set.Iio a = Set.Ico a b

theorem Set.Ioi_injective {α : Type u_1} [LinearOrder α] : Function.Injective Set.Ioi

theorem Set.Iio_injective {α : Type u_1} [LinearOrder α] : Function.Injective Set.Iio

theorem Set.Ioi_inj {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a = Set.Ioi b ↔ a = b

theorem Set.Iio_inj {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio a = Set.Iio b ↔ a = b

theorem Set.Ico_subset_Ico_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) : Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

theorem Set.Ioc_subset_Ioc_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ < b₁) : Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

theorem Set.Ioo_subset_Ioo_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} [DenselyOrdered α] (h₁ : a₁ < b₁) : Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

theorem Set.Ico_eq_Ico_iff {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : a₁ < b₁ ∨ a₂ < b₂) : Set.Ico a₁ b₁ = Set.Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

theorem Set.Ici_eq_singleton_iff_isTop {α : Type u_1} [LinearOrder α] {x : α} : Set.Ici x = {x} ↔ IsTop x

@[simp]

theorem Set.Ioi_subset_Ioi_iff {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi b ⊆ Set.Ioi a ↔ a ≤ b

@[simp]

theorem Set.Ioi_subset_Ici_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] : Set.Ioi b ⊆ Set.Ici a ↔ a ≤ b

@[simp]

theorem Set.Iio_subset_Iio_iff {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio a ⊆ Set.Iio b ↔ a ≤ b

@[simp]

theorem Set.Iio_subset_Iic_iff {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] : Set.Iio a ⊆ Set.Iic b ↔ a ≤ b

Unions of adjacent intervals

Two infinite intervals

theorem Set.Iic_union_Ioi_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iic b ∪ Set.Ioi a = Set.univ

theorem Set.Iio_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iio b ∪ Set.Ici a = Set.univ

theorem Set.Iic_union_Ici_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iic b ∪ Set.Ici a = Set.univ

theorem Set.Iio_union_Ioi_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Set.Iio b ∪ Set.Ioi a = Set.univ

@[simp]

theorem Set.Iic_union_Ici {α : Type u_1} [LinearOrder α] {a : α} : Set.Iic a ∪ Set.Ici a = Set.univ

@[simp]

theorem Set.Iio_union_Ici {α : Type u_1} [LinearOrder α] {a : α} : Set.Iio a ∪ Set.Ici a = Set.univ

@[simp]

theorem Set.Iic_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} : Set.Iic a ∪ Set.Ioi a = Set.univ

@[simp]

theorem Set.Iio_union_Ioi {α : Type u_1} [LinearOrder α] {a : α} : Set.Iio a ∪ Set.Ioi a = {a}ᶜ

A finite and an infinite interval

theorem Set.Ioo_union_Ioi' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c < b) : Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (a ⊓ c)

theorem Set.Ioo_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c < a ⊔ b) : Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (a ⊓ c)

theorem Set.Ioi_subset_Ioo_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a ⊆ Set.Ioo a b ∪ Set.Ici b

@[simp]

theorem Set.Ioo_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Set.Ioo a b ∪ Set.Ici b = Set.Ioi a

theorem Set.Ici_subset_Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ici a ⊆ Set.Ico a b ∪ Set.Ici b

@[simp]

theorem Set.Ico_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Ico a b ∪ Set.Ici b = Set.Ici a

theorem Set.Ico_union_Ici' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Set.Ico a b ∪ Set.Ici c = Set.Ici (a ⊓ c)

theorem Set.Ico_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) : Set.Ico a b ∪ Set.Ici c = Set.Ici (a ⊓ c)

theorem Set.Ioi_subset_Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ioi b

@[simp]

theorem Set.Ioc_union_Ioi_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Ioc a b ∪ Set.Ioi b = Set.Ioi a

theorem Set.Ioc_union_Ioi' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (a ⊓ c)

theorem Set.Ioc_union_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) : Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (a ⊓ c)

theorem Set.Ici_subset_Icc_union_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ici a ⊆ Set.Icc a b ∪ Set.Ioi b

@[simp]

theorem Set.Icc_union_Ioi_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Icc a b ∪ Set.Ioi b = Set.Ici a

theorem Set.Ioi_subset_Ioc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ici b

@[simp]

theorem Set.Ioc_union_Ici_eq_Ioi {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Set.Ioc a b ∪ Set.Ici b = Set.Ioi a

theorem Set.Ici_subset_Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ici a ⊆ Set.Icc a b ∪ Set.Ici b

@[simp]

theorem Set.Icc_union_Ici_eq_Ici {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Icc a b ∪ Set.Ici b = Set.Ici a

theorem Set.Icc_union_Ici' {α : Type u_1} [LinearOrder α] {a b c : α} (h₁ : c ≤ b) : Set.Icc a b ∪ Set.Ici c = Set.Ici (a ⊓ c)

theorem Set.Icc_union_Ici {α : Type u_1} [LinearOrder α] {a b c : α} (h : c ≤ a ⊔ b) : Set.Icc a b ∪ Set.Ici c = Set.Ici (a ⊓ c)

An infinite and a finite interval

theorem Set.Iic_subset_Iio_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iic b ⊆ Set.Iio a ∪ Set.Icc a b

@[simp]

theorem Set.Iio_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iio a ∪ Set.Icc a b = Set.Iic b

theorem Set.Iio_subset_Iio_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio b ⊆ Set.Iio a ∪ Set.Ico a b

@[simp]

theorem Set.Iio_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iio a ∪ Set.Ico a b = Set.Iio b

theorem Set.Iio_union_Ico' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c ≤ b) : Set.Iio b ∪ Set.Ico c d = Set.Iio (b ⊔ d)

theorem Set.Iio_union_Ico {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d ≤ b) : Set.Iio b ∪ Set.Ico c d = Set.Iio (b ⊔ d)

theorem Set.Iic_subset_Iic_union_Ioc {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iic b ⊆ Set.Iic a ∪ Set.Ioc a b

@[simp]

theorem Set.Iic_union_Ioc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iic a ∪ Set.Ioc a b = Set.Iic b

theorem Set.Iic_union_Ioc' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c < b) : Set.Iic b ∪ Set.Ioc c d = Set.Iic (b ⊔ d)

theorem Set.Iic_union_Ioc {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d < b) : Set.Iic b ∪ Set.Ioc c d = Set.Iic (b ⊔ d)

theorem Set.Iio_subset_Iic_union_Ioo {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio b ⊆ Set.Iic a ∪ Set.Ioo a b

@[simp]

theorem Set.Iic_union_Ioo_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : Set.Iic a ∪ Set.Ioo a b = Set.Iio b

theorem Set.Iio_union_Ioo' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c < b) : Set.Iio b ∪ Set.Ioo c d = Set.Iio (b ⊔ d)

theorem Set.Iio_union_Ioo {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d < b) : Set.Iio b ∪ Set.Ioo c d = Set.Iio (b ⊔ d)

theorem Set.Iic_subset_Iic_union_Icc {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iic b ⊆ Set.Iic a ∪ Set.Icc a b

@[simp]

theorem Set.Iic_union_Icc_eq_Iic {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.Iic a ∪ Set.Icc a b = Set.Iic b

theorem Set.Iic_union_Icc' {α : Type u_1} [LinearOrder α] {b c d : α} (h₁ : c ≤ b) : Set.Iic b ∪ Set.Icc c d = Set.Iic (b ⊔ d)

theorem Set.Iic_union_Icc {α : Type u_1} [LinearOrder α] {b c d : α} (h : c ⊓ d ≤ b) : Set.Iic b ∪ Set.Icc c d = Set.Iic (b ⊔ d)

theorem Set.Iio_subset_Iic_union_Ico {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio b ⊆ Set.Iic a ∪ Set.Ico a b

@[simp]

theorem Set.Iic_union_Ico_eq_Iio {α : Type u_1} [LinearOrder α] {a b : α} (h : 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_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : Set.Ioo a b ∪ Set.Ico b c = Set.Ioo a c

theorem Set.Ico_subset_Ico_union_Ico {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Set.Ico a b ∪ Set.Ico b c = Set.Ico a c

theorem Set.Ico_union_Ico' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) : Set.Ico a b ∪ Set.Ico c d = Set.Ico (a ⊓ c) (b ⊔ d)

theorem Set.Ico_union_Ico {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b ≤ c ⊔ d) (h₂ : c ⊓ d ≤ a ⊔ b) : Set.Ico a b ∪ Set.Ico c d = Set.Ico (a ⊓ c) (b ⊔ d)

theorem Set.Icc_subset_Ico_union_Icc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Set.Ico a b ∪ Set.Icc b c = Set.Icc a c

theorem Set.Ioc_subset_Ioo_union_Icc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {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?

theorem Set.Ioo_subset_Ioc_union_Ioo {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : Set.Ioc a b ∪ Set.Ioo b c = Set.Ioo a c

theorem Set.Ico_subset_Icc_union_Ioo {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : Set.Icc a b ∪ Set.Ioo b c = Set.Ico a c

theorem Set.Icc_subset_Icc_union_Ioc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Set.Icc a b ∪ Set.Ioc b c = Set.Icc a c

theorem Set.Ioc_subset_Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c

theorem Set.Ioc_union_Ioc' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) : Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (a ⊓ c) (b ⊔ d)

theorem Set.Ioc_union_Ioc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b ≤ c ⊔ d) (h₂ : c ⊓ d ≤ a ⊔ b) : Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (a ⊓ c) (b ⊔ d)

Two finite intervals with a common point

theorem Set.Ioo_subset_Ioc_union_Ico {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) : Set.Ioc a b ∪ Set.Ico b c = Set.Ioo a c

theorem Set.Ico_subset_Icc_union_Ico {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : Set.Icc a b ∪ Set.Ico b c = Set.Ico a c

theorem Set.Icc_subset_Icc_union_Icc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Set.Icc a b ∪ Set.Icc b c = Set.Icc a c

theorem Set.Icc_union_Icc' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c ≤ b) (h₂ : a ≤ d) : Set.Icc a b ∪ Set.Icc c d = Set.Icc (a ⊓ c) (b ⊔ d)

theorem Set.Icc_union_Icc {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b < c ⊔ d) (h₂ : c ⊓ d < a ⊔ b) : Set.Icc a b ∪ Set.Icc c d = Set.Icc (a ⊓ c) (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}.

theorem Set.Ioc_subset_Ioc_union_Icc {α : Type u_1} [LinearOrder α] {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_1} [LinearOrder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : Set.Ioc a b ∪ Set.Icc b c = Set.Ioc a c

theorem Set.Ioo_union_Ioo' {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : c < b) (h₂ : a < d) : Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (a ⊓ c) (b ⊔ d)

theorem Set.Ioo_union_Ioo {α : Type u_1} [LinearOrder α] {a b c d : α} (h₁ : a ⊓ b < c ⊔ d) (h₂ : c ⊓ d < a ⊔ b) : Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (a ⊓ c) (b ⊔ d)

theorem Set.Ioo_subset_Ioo_union_Ioo {α : Type u_1} [LinearOrder α] {a a₁ b b₁ c d : α} (h₁ : a ≤ a₁) (h₂ : c < b) (h₃ : b₁ ≤ d) : Set.Ioo a₁ b₁ ⊆ Set.Ioo a b ∪ Set.Ioo c d

@[simp]

theorem Set.Iic_inter_Iic {α : Type u_1} [SemilatticeInf α] {a b : α} : Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)

@[simp]

theorem Set.Ioc_inter_Iic {α : Type u_1} [SemilatticeInf α] (a b c : α) : Set.Ioc a b ∩ Set.Iic c = Set.Ioc a (b ⊓ c)

@[simp]

theorem Set.Ici_inter_Ici {α : Type u_1} [SemilatticeSup α] {a b : α} : Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)

@[simp]

theorem Set.Ico_inter_Ici {α : Type u_1} [SemilatticeSup α] (a b c : α) : Set.Ico a b ∩ Set.Ici c = Set.Ico (a ⊔ c) b

theorem Set.Icc_inter_Icc {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} : Set.Icc a₁ b₁ ∩ Set.Icc a₂ b₂ = Set.Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

@[simp]

theorem Set.Icc_inter_Icc_eq_singleton {α : Type u_1} [Lattice α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Set.Icc a b ∩ Set.Icc b c = {b}

@[simp]

theorem Set.Ioi_inter_Ioi {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioi a ∩ Set.Ioi b = Set.Ioi (a ⊔ b)

@[simp]

theorem Set.Iio_inter_Iio {α : Type u_1} [LinearOrder α] {a b : α} : Set.Iio a ∩ Set.Iio b = Set.Iio (a ⊓ b)

theorem Set.Ico_inter_Ico {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Set.Ico a₁ b₁ ∩ Set.Ico a₂ b₂ = Set.Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)

theorem Set.Ioc_inter_Ioc {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Set.Ioc a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

theorem Set.Ioo_inter_Ioo {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Set.Ioo a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)

theorem Set.Ioo_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioo a b ∩ Set.Iio c = Set.Ioo a (b ⊓ c)

theorem Set.Iio_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Iio a ∩ Set.Ioo b c = Set.Ioo b (a ⊓ c)

theorem Set.Ioo_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioo a b ∩ Set.Ioi c = Set.Ioo (a ⊔ c) b

theorem Set.Ioi_inter_Ioo {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (a ⊔ b) c

theorem Set.Ioc_inter_Ioo_of_left_lt {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₁ < b₂) : Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioc (a₁ ⊔ a₂) b₁

theorem Set.Ioc_inter_Ioo_of_right_le {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₂ ≤ b₁) : Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (a₁ ⊔ a₂) b₂

theorem Set.Ioo_inter_Ioc_of_left_le {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₁ ≤ b₂) : Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioo (a₁ ⊔ a₂) b₁

theorem Set.Ioo_inter_Ioc_of_right_lt {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (h : b₂ < b₁) : Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (a₁ ⊔ a₂) b₂

@[simp]

theorem Set.Ico_diff_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ico a b \ Set.Iio c = Set.Ico (a ⊔ c) b

@[simp]

theorem Set.Ioc_diff_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a b \ Set.Ioi c = Set.Ioc a (b ⊓ c)

@[simp]

theorem Set.Ioc_inter_Ioi {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a b ∩ Set.Ioi c = Set.Ioc (a ⊔ c) b

@[simp]

theorem Set.Ico_inter_Iio {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ico a b ∩ Set.Iio c = Set.Ico a (b ⊓ c)

@[simp]

theorem Set.Ioc_diff_Iic {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a b \ Set.Iic c = Set.Ioc (a ⊔ c) b

@[simp]

theorem Set.Ioc_union_Ioc_right {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a b ∪ Set.Ioc a c = Set.Ioc a (b ⊔ c)

@[simp]

theorem Set.Ioc_union_Ioc_left {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a c ∪ Set.Ioc b c = Set.Ioc (a ⊓ b) c

@[simp]

theorem Set.Ioc_union_Ioc_symm {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioc a b ∪ Set.Ioc b a = Set.Ioc (a ⊓ b) (a ⊔ b)

@[simp]

theorem Set.Ioc_union_Ioc_union_Ioc_cycle {α : Type u_1} [LinearOrder α] {a b c : α} : Set.Ioc a b ∪ Set.Ioc b c ∪ Set.Ioc c a = Set.Ioc (a ⊓ (b ⊓ c)) (a ⊔ (b ⊔ c))

Closed intervals in α × β

@[simp]

theorem Set.Iic_prod_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Set.Iic a ×ˢ Set.Iic b = Set.Iic (a, b)

@[simp]

theorem Set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Set.Ici a ×ˢ Set.Ici b = Set.Ici (a, b)

theorem Set.Ici_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Set.Ici a = Set.Ici a.fst ×ˢ Set.Ici a.snd

theorem Set.Iic_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Set.Iic a = Set.Iic a.fst ×ˢ Set.Iic a.snd

@[simp]

theorem Set.Icc_prod_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) : Set.Icc a₁ a₂ ×ˢ Set.Icc b₁ b₂ = Set.Icc (a₁, b₁) (a₂, b₂)

theorem Set.Icc_prod_eq {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a b : α × β) : Set.Icc a b = Set.Icc a.fst b.fst ×ˢ Set.Icc a.snd b.snd

Lemmas about intervals in dense orders

instance instNoMinOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMinOrder ↑(Set.Ioo x y)

Equations

• ⋯ = ⋯

instance instNoMinOrderElemIoc (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMinOrder ↑(Set.Ioc x y)

Equations

• ⋯ = ⋯

instance instNoMinOrderElemIoi (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} : NoMinOrder ↑(Set.Ioi x)

Equations

• ⋯ = ⋯

instance instNoMaxOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMaxOrder ↑(Set.Ioo x y)

Equations

• ⋯ = ⋯

instance instNoMaxOrderElemIco (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} : NoMaxOrder ↑(Set.Ico x y)

Equations

• ⋯ = ⋯

instance instNoMaxOrderElemIio (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} : NoMaxOrder ↑(Set.Iio x)

Equations

• ⋯ = ⋯

Intervals in Prop

@[simp]

theorem Set.Iic_False : Set.Iic False = {False}

@[simp]

theorem Set.Iic_True : Set.Iic True = Set.univ

@[simp]

theorem Set.Ici_False : Set.Ici False = Set.univ

@[simp]

theorem Set.Ici_True : Set.Ici True = {True}

@[simp]

theorem Set.Iio_False : Set.Iio False = ∅

@[simp]

theorem Set.Iio_True : Set.Iio True = {False}

@[simp]

theorem Set.Ioi_False : Set.Ioi False = {True}

@[simp]

theorem Set.Ioi_True : Set.Ioi True = ∅