Documentation

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

This file contains basic facts on inclusion of and set operations on intervals (where the precise statements depend on the order's properties; statements requiring LinearOrder are in Mathlib/Order/Interval/Set/LinearOrder.lean).

A conscious decision was made not to list all possible inclusion relations. Monotonicity results and "self" results are included. Most use cases can suffice with a transitive combination of those, for example:

theorem Ico_subset_Ici (h : a₂ ≤ a₁) : Ico a₁ b₁ ⊆ Ici a₂ :=
  (Ico_subset_Ico_left h).trans Ico_subset_Ici_self

Logical equivalences, such as Icc_subset_Ici_iff, are however stated.

source
instance Set.decidableMemIoo {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x ∧ x < b)] :
Decidable (x ∈ Ioo a b)
Equations
source
instance Set.decidableMemIco {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x ∧ x < b)] :
Decidable (x ∈ Ico a b)
Equations
source
instance Set.decidableMemIio {α : Type u_1} [Preorder α] {b x : α} [Decidable (x < b)] :
Decidable (x ∈ Iio b)
Equations
source
instance Set.decidableMemIcc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a ≤ x ∧ x ≤ b)] :
Decidable (x ∈ Icc a b)
Equations
source
instance Set.decidableMemIic {α : Type u_1} [Preorder α] {b x : α} [Decidable (x ≤ b)] :
Decidable (x ∈ Iic b)
Equations
source
instance Set.decidableMemIoc {α : Type u_1} [Preorder α] {a b x : α} [Decidable (a < x ∧ x ≤ b)] :
Decidable (x ∈ Ioc a b)
Equations
source
instance Set.decidableMemIci {α : Type u_1} [Preorder α] {a x : α} [Decidable (a ≤ x)] :
Decidable (x ∈ Ici a)
Equations
source
instance Set.decidableMemIoi {α : Type u_1} [Preorder α] {a x : α} [Decidable (a < x)] :
Decidable (x ∈ Ioi a)
Equations
source
theorem Set.left_notMem_Ioo {α : Type u_1} [Preorder α] (a b : α) :
a ∉ Ioo a b
source
theorem Set.left_notMem_Ioc {α : Type u_1} [Preorder α] (a b : α) :
a ∉ Ioc a b
source
@[deprecated Set.left_notMem_Ioo (since := "2025-12-26")]
theorem Set.left_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} :
a ∈ Ioo a b ↔ False
source
@[deprecated Set.left_notMem_Ioc (since := "2025-12-26")]
theorem Set.left_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} :
a ∈ Ioc a b ↔ False
source
theorem Set.left_mem_Ico {α : Type u_1} [Preorder α] {a b : α} :
a ∈ Ico a b ↔ a < b
source
theorem Set.left_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :
a ∈ Icc a b ↔ a ≤ b
source
theorem Set.self_notMem_Ioi {α : Type u_1} [Preorder α] {a : α} :
a ∉ Ioi a
source
theorem Set.self_mem_Ici {α : Type u_1} [Preorder α] {a : α} :
a ∈ Ici a
source
@[deprecated Set.self_mem_Ici (since := "2025-12-26")]
theorem Set.left_mem_Ici {α : Type u_1} [Preorder α] {a : α} :
a ∈ Ici a

Alias of Set.self_mem_Ici.

source
theorem Set.right_notMem_Ioo {α : Type u_1} [Preorder α] {a b : α} :
b ∉ Ioo a b
source
theorem Set.right_notMem_Ico {α : Type u_1} [Preorder α] {a b : α} :
b ∉ Ico a b
source
@[deprecated Set.right_notMem_Ioo (since := "2025-12-26")]
theorem Set.right_mem_Ioo {α : Type u_1} [Preorder α] {a b : α} :
b ∈ Ioo a b ↔ False
source
@[deprecated Set.right_notMem_Ico (since := "2025-12-26")]
theorem Set.right_mem_Ico {α : Type u_1} [Preorder α] {a b : α} :
b ∈ Ico a b ↔ False
source
theorem Set.right_mem_Ioc {α : Type u_1} [Preorder α] {a b : α} :
b ∈ Ioc a b ↔ a < b
source
theorem Set.right_mem_Icc {α : Type u_1} [Preorder α] {a b : α} :
b ∈ Icc a b ↔ a ≤ b
source
theorem Set.self_notMem_Iio {α : Type u_1} [Preorder α] {a : α} :
a ∉ Iio a
source
theorem Set.self_mem_Iic {α : Type u_1} [Preorder α] {a : α} :
a ∈ Iic a
source
@[deprecated Set.self_mem_Iic (since := "2025-12-26")]
theorem Set.right_mem_Iic {α : Type u_1} [Preorder α] {a : α} :
a ∈ Iic a

Alias of Set.self_mem_Iic.

source
@[simp]
theorem Set.Ici_toDual {α : Type u_1} [Preorder α] {a : α} :
Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Iic a
source
@[simp]
theorem Set.Iic_toDual {α : Type u_1} [Preorder α] {a : α} :
Iic (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Ici a
source
@[simp]
theorem Set.Ioi_toDual {α : Type u_1} [Preorder α] {a : α} :
Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Iio a
source
@[simp]
theorem Set.Iio_toDual {α : Type u_1} [Preorder α] {a : α} :
Iio (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Ioi a
source
@[simp]
theorem Set.Icc_toDual {α : Type u_1} [Preorder α] {a b : α} :
Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Icc b a
source
@[simp]
theorem Set.Ioc_toDual {α : Type u_1} [Preorder α] {a b : α} :
Ioc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ico b a
source
@[simp]
theorem Set.Ico_toDual {α : Type u_1} [Preorder α] {a b : α} :
Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ioc b a
source
@[simp]
theorem Set.Ioo_toDual {α : Type u_1} [Preorder α] {a b : α} :
Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Ioo b a
source
@[simp]
theorem Set.Ici_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} :
Ici (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Iic x
source
@[simp]
theorem Set.Iic_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} :
Iic (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ici x
source
@[simp]
theorem Set.Ioi_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} :
Ioi (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Iio x
source
@[simp]
theorem Set.Iio_ofDual {α : Type u_1} [Preorder α] {x : αᵒᵈ} :
Iio (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioi x
source
@[simp]
theorem Set.Icc_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} :
Icc (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Icc x y
source
@[simp]
theorem Set.Ico_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} :
Ico (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioc x y
source
@[simp]
theorem Set.Ioc_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} :
Ioc (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ico x y
source
@[simp]
theorem Set.Ioo_ofDual {α : Type u_1} [Preorder α] {x y : αᵒᵈ} :
Ioo (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Ioo x y
source
@[simp]
theorem Set.nonempty_Icc {α : Type u_1} [Preorder α] {a b : α} :
(Icc a b).Nonempty ↔ a ≤ b
source
@[simp]
theorem Set.nonempty_Ico {α : Type u_1} [Preorder α] {a b : α} :
(Ico a b).Nonempty ↔ a < b
source
@[simp]
theorem Set.nonempty_Ioc {α : Type u_1} [Preorder α] {a b : α} :
(Ioc a b).Nonempty ↔ a < b
source
@[simp]
theorem Set.nonempty_Ici {α : Type u_1} [Preorder α] {a : α} :
(Ici a).Nonempty
source
@[simp]
theorem Set.nonempty_Iic {α : Type u_1} [Preorder α] {a : α} :
(Iic a).Nonempty
source
@[simp]
theorem Set.nonempty_Ioo {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] :
(Ioo a b).Nonempty ↔ a < b
source
@[simp]
theorem Set.nonempty_Ioi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
(Ioi a).Nonempty
source
@[simp]
theorem Set.nonempty_Iio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
(Iio a).Nonempty
source
theorem Set.nonempty_Icc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :
Nonempty ↑(Icc a b)
source
theorem Set.nonempty_Ico_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
Nonempty ↑(Ico a b)
source
theorem Set.nonempty_Ioc_subtype {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
Nonempty ↑(Ioc a b)
source
instance Set.nonempty_Ici_subtype {α : Type u_1} [Preorder α] {a : α} :
Nonempty ↑(Ici a)

An interval Ici a is nonempty.

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

An interval Iic a is nonempty.

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

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

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

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

source
instance Set.instNoMinOrderElemIio {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
NoMinOrder ↑(Iio a)
source
instance Set.instNoMinOrderElemIic {α : Type u_1} [Preorder α] {a : α} [NoMinOrder α] :
NoMinOrder ↑(Iic a)
source
instance Set.instNoMaxOrderElemIoi {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
NoMaxOrder ↑(Ioi a)
source
instance Set.instNoMaxOrderElemIci {α : Type u_1} [Preorder α] {a : α} [NoMaxOrder α] :
NoMaxOrder ↑(Ici a)
source
@[simp]
theorem Set.Icc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a ≤ b) :
Icc a b = ∅
source
@[simp]
theorem Set.Ico_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
Ico a b = ∅
source
@[simp]
theorem Set.Ioc_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
Ioc a b = ∅
source
@[simp]
theorem Set.Ioo_eq_empty {α : Type u_1} [Preorder α] {a b : α} (h : ¬a < b) :
Ioo a b = ∅
source
@[simp]
theorem Set.Icc_eq_empty_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) :
Icc a b = ∅
source
@[simp]
theorem Set.Ico_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) :
Ico a b = ∅
source
@[simp]
theorem Set.Ioc_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) :
Ioc a b = ∅
source
@[simp]
theorem Set.Ioo_eq_empty_of_le {α : Type u_1} [Preorder α] {a b : α} (h : b ≤ a) :
Ioo a b = ∅
source
theorem Set.Ico_self {α : Type u_1} [Preorder α] (a : α) :
Ico a a = ∅
source
theorem Set.Ioc_self {α : Type u_1} [Preorder α] (a : α) :
Ioc a a = ∅
source
theorem Set.Ioo_self {α : Type u_1} [Preorder α] (a : α) :
Ioo a a = ∅
source
@[simp]
theorem Set.Ici_subset_Ici {α : Type u_1} [Preorder α] {a b : α} :
Ici a ⊆ Ici b ↔ b ≤ a
source
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.

source
@[simp]
theorem Set.Ici_ssubset_Ici {α : Type u_1} [Preorder α] {a b : α} :
Ici a ⊂ Ici b ↔ b < a
source
theorem GCongr.Ici_ssubset_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_ssubset_Ici.

source
@[simp]
theorem Set.Iic_subset_Iic {α : Type u_1} [Preorder α] {a b : α} :
Iic a ⊆ Iic b ↔ a ≤ b
source
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.

source
@[simp]
theorem Set.Iic_ssubset_Iic {α : Type u_1} [Preorder α] {a b : α} :
Iic a ⊂ Iic b ↔ a < b
source
theorem GCongr.Iic_ssubset_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_ssubset_Iic.

source
@[simp]
theorem Set.Ici_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} :
Ici a ⊆ Ioi b ↔ b < a
source
@[simp]
theorem Set.Iic_subset_Iio {α : Type u_1} [Preorder α] {a b : α} :
Iic a ⊆ Iio b ↔ a < b
source
theorem Set.Ioo_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
Ioo a₁ b₁ ⊆ Ioo a₂ b₂
source
theorem Set.Ioo_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
Ioo a₂ b ⊆ Ioo a₁ b
source
theorem Set.Ioo_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
Ioo a b₁ ⊆ Ioo a b₂
source
theorem Set.Ico_subset_Ico {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
Ico a₁ b₁ ⊆ Ico a₂ b₂
source
theorem Set.Ico_subset_Ico_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
Ico a₂ b ⊆ Ico a₁ b
source
theorem Set.Ico_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
Ico a b₁ ⊆ Ico a b₂
source
theorem Set.Icc_subset_Icc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
Icc a₁ b₁ ⊆ Icc a₂ b₂
source
theorem Set.Icc_subset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
Icc a₂ b ⊆ Icc a₁ b
source
theorem Set.Icc_subset_Icc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
Icc a b₁ ⊆ Icc a b₂
source
theorem Set.Icc_subset_Ioo {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ < a₁) (hb : b₁ < b₂) :
Icc a₁ b₁ ⊆ Ioo a₂ b₂
source
theorem Set.Icc_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} :
Icc a b ⊆ Ici a
source
theorem Set.Icc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} :
Icc a b ⊆ Iic b
source
theorem Set.Ioc_subset_Iic_self {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b ⊆ Iic b
source
theorem Set.Ioc_subset_Ioc {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
Ioc a₁ b₁ ⊆ Ioc a₂ b₂
source
theorem Set.Ioc_subset_Ioc_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h : a₁ ≤ a₂) :
Ioc a₂ b ⊆ Ioc a₁ b
source
theorem Set.Ioc_subset_Ioc_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ ≤ b₂) :
Ioc a b₁ ⊆ Ioc a b₂
source
theorem Set.Ico_subset_Ioo_left {α : Type u_1} [Preorder α] {a₁ a₂ b : α} (h₁ : a₁ < a₂) :
Ico a₂ b ⊆ Ioo a₁ b
source
theorem Set.Ioc_subset_Ioo_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
Ioc a b₁ ⊆ Ioo a b₂
source
theorem Set.Icc_subset_Ico_right {α : Type u_1} [Preorder α] {a b₁ b₂ : α} (h₁ : b₁ < b₂) :
Icc a b₁ ⊆ Ico a b₂
source
theorem Set.Ioo_subset_Ico_self {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b ⊆ Ico a b
source
theorem Set.Ioo_subset_Ioc_self {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b ⊆ Ioc a b
source
theorem Set.Ico_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
Ico a b ⊆ Icc a b
source
theorem Set.Ioc_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b ⊆ Icc a b
source
theorem Set.Ioo_subset_Icc_self {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b ⊆ Icc a b
source
theorem Set.Ico_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} :
Ico a b ⊆ Iio b
source
theorem Set.Ioo_subset_Iio_self {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b ⊆ Iio b
source
theorem Set.Ioc_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b ⊆ Ioi a
source
theorem Set.Ioo_subset_Ioi_self {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b ⊆ Ioi a
source
theorem Set.Ioi_subset_Ici_self {α : Type u_1} [Preorder α] {a : α} :
Ioi a ⊆ Ici a
source
theorem Set.Iio_subset_Iic_self {α : Type u_1} [Preorder α] {a : α} :
Iio a ⊆ Iic a
source
theorem Set.Ico_subset_Ici_self {α : Type u_1} [Preorder α] {a b : α} :
Ico a b ⊆ Ici a
source
theorem Set.Ioi_ssubset_Ici_self {α : Type u_1} [Preorder α] {a : α} :
Ioi a ⊂ Ici a
source
theorem Set.Iio_ssubset_Iic_self {α : Type u_1} [Preorder α] {a : α} :
Iio a ⊂ Iic a
source
theorem Set.Icc_subset_Icc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
theorem Set.Icc_subset_Ioo_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
source
theorem Set.Icc_subset_Ico_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
source
theorem Set.Icc_subset_Ioc_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂
source
theorem Set.Icc_subset_Iio_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Iio b₂ ↔ b₁ < b₂
source
theorem Set.Icc_subset_Ioi_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁
source
theorem Set.Icc_subset_Iic_iff {α : Type u_1} [Preorder α] {a₁ b₁ b₂ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Iic b₂ ↔ b₁ ≤ b₂
source
theorem Set.Icc_subset_Ici_iff {α : Type u_1} [Preorder α] {a₁ a₂ b₁ : α} (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ici a₂ ↔ a₂ ≤ a₁
source
theorem Set.Icc_ssubset_Icc_left {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) :
Icc a₁ b₁ ⊂ Icc a₂ b₂
source
theorem Set.Icc_ssubset_Icc_right {α : Type u_1} [Preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) :
Icc a₁ b₁ ⊂ Icc a₂ b₂
source
theorem Set.Ioi_subset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :
Ioi b ⊆ 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_ssubset_Ioi {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
Ioi b ⊂ 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_ssubset_Ioi_iff.

source
theorem Set.Ioi_subset_Ici {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :
Ioi b ⊆ Ici a

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

source
theorem Set.Iio_subset_Iio {α : Type u_1} [Preorder α] {a b : α} (h : a ≤ b) :
Iio a ⊆ 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_ssubset_Iio {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
Iio a ⊂ 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_ssubset_Iio_iff.

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

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

source
theorem Set.Ici_inter_Iic {α : Type u_1} [Preorder α] {a b : α} :
Ici a ∩ Iic b = Icc a b
source
theorem Set.Ici_inter_Iio {α : Type u_1} [Preorder α] {a b : α} :
Ici a ∩ Iio b = Ico a b
source
theorem Set.Ioi_inter_Iic {α : Type u_1} [Preorder α] {a b : α} :
Ioi a ∩ Iic b = Ioc a b
source
theorem Set.Ioi_inter_Iio {α : Type u_1} [Preorder α] {a b : α} :
Ioi a ∩ Iio b = Ioo a b
source
theorem Set.Iic_inter_Ici {α : Type u_1} [Preorder α] {a b : α} :
Iic a ∩ Ici b = Icc b a
source
theorem Set.Iio_inter_Ici {α : Type u_1} [Preorder α] {a b : α} :
Iio a ∩ Ici b = Ico b a
source
theorem Set.Iic_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} :
Iic a ∩ Ioi b = Ioc b a
source
theorem Set.Iio_inter_Ioi {α : Type u_1} [Preorder α] {a b : α} :
Iio a ∩ Ioi b = Ioo b a
source
theorem Set.mem_Icc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ioo a b) :
x ∈ Icc a b
source
theorem Set.mem_Ico_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ioo a b) :
x ∈ Ico a b
source
theorem Set.mem_Ioc_of_Ioo {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ioo a b) :
x ∈ Ioc a b
source
theorem Set.mem_Icc_of_Ico {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ico a b) :
x ∈ Icc a b
source
theorem Set.mem_Icc_of_Ioc {α : Type u_1} [Preorder α] {a b x : α} (h : x ∈ Ioc a b) :
x ∈ Icc a b
source
theorem Set.mem_Ici_of_Ioi {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Ioi a) :
x ∈ Ici a
source
theorem Set.mem_Iic_of_Iio {α : Type u_1} [Preorder α] {a x : α} (h : x ∈ Iio a) :
x ∈ Iic a
source
theorem Set.Icc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
Icc a b = ∅ ↔ ¬a ≤ b
source
theorem Set.Ico_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
Ico a b = ∅ ↔ ¬a < b
source
theorem Set.Ioc_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b = ∅ ↔ ¬a < b
source
theorem Set.Ioo_eq_empty_iff {α : Type u_1} [Preorder α] {a b : α} [DenselyOrdered α] :
Ioo a b = ∅ ↔ ¬a < b
source
theorem IsTop.Iic_eq {α : Type u_1} [Preorder α] {a : α} (h : IsTop a) :
Set.Iic a = Set.univ
source
theorem IsBot.Ici_eq {α : Type u_1} [Preorder α] {a : α} (h : IsBot a) :
Set.Ici a = Set.univ
source
@[simp]
theorem Set.Ioi_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} :
Ioi a = ∅ ↔ IsMax a
source
@[simp]
theorem Set.Iio_eq_empty_iff {α : Type u_1} [Preorder α] {a : α} :
Iio a = ∅ ↔ IsMin a
source
@[simp]
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.

source
@[simp]
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.

source
@[simp]
theorem Set.Iio_nonempty {α : Type u_1} [Preorder α] {a : α} :
(Iio a).Nonempty ↔ ¬IsMin a
source
@[simp]
theorem Set.Ioi_nonempty {α : Type u_1} [Preorder α] {a : α} :
(Ioi a).Nonempty ↔ ¬IsMax a
source
theorem Set.Iic_inter_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (h : a ≤ c) :
Iic a ∩ Ioc b c = Ioc b a
source
theorem Set.notMem_Icc_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
c ∉ Icc a b
source
theorem Set.notMem_Icc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
c ∉ Icc a b
source
theorem Set.notMem_Ico_of_lt {α : Type u_1} [Preorder α] {a b c : α} (ha : c < a) :
c ∉ Ico a b
source
theorem Set.notMem_Ioc_of_gt {α : Type u_1} [Preorder α] {a b c : α} (hb : b < c) :
c ∉ Ioc a b
source
theorem Set.notMem_Ioi_self {α : Type u_1} [Preorder α] {a : α} :
a ∉ Ioi a
source
theorem Set.notMem_Iio_self {α : Type u_1} [Preorder α] {b : α} :
b ∉ Iio b
source
theorem Set.notMem_Ioc_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) :
c ∉ Ioc a b
source
theorem Set.notMem_Ico_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b ≤ c) :
c ∉ Ico a b
source
theorem Set.notMem_Ioo_of_le {α : Type u_1} [Preorder α] {a b c : α} (ha : c ≤ a) :
c ∉ Ioo a b
source
theorem Set.notMem_Ioo_of_ge {α : Type u_1} [Preorder α] {a b c : α} (hb : b ≤ c) :
c ∉ Ioo a b
source
@[simp]
theorem Set.Icc_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Icc a b = Ioc a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Icc_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Icc a b = Ico a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Icc_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Icc a b = Ioo a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Ioc_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b = Ico a b ↔ ¬a < b
source
@[simp]
theorem Set.Ioo_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b = Ioc a b ↔ ¬a < b
source
@[simp]
theorem Set.Ioo_eq_Ico_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b = Ico a b ↔ ¬a < b
source
@[simp]
theorem Set.Ioc_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b = Icc a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Ico_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ico a b = Icc a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Ioo_eq_Icc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioo a b = Icc a b ↔ ¬a ≤ b
source
@[simp]
theorem Set.Ico_eq_Ioc_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ico a b = Ioc a b ↔ ¬a < b
source
@[simp]
theorem Set.Ioc_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ioc a b = Ioo a b ↔ ¬a < b
source
@[simp]
theorem Set.Ico_eq_Ioo_same_iff {α : Type u_1} [Preorder α] {a b : α} :
Ico a b = Ioo a b ↔ ¬a < b
source
@[simp]
theorem Set.Icc_self {α : Type u_1} [PartialOrder α] (a : α) :
Icc a a = {a}
source
instance Set.instIccUnique {α : Type u_1} [PartialOrder α] {a : α} :
Unique ↑(Icc a a)
Equations
source
@[simp]
theorem Set.Icc_eq_singleton_iff {α : Type u_1} [PartialOrder α] {a b c : α} :
Icc a b = {c} ↔ a = c ∧ b = c
source
theorem Set.subsingleton_Icc_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (hba : b ≤ a) :
(Icc a b).Subsingleton
source
@[simp]
theorem Set.subsingleton_Icc_iff {α : Type u_2} [LinearOrder α] {a b : α} :
(Icc a b).Subsingleton ↔ b ≤ a
source
@[simp]
theorem Set.Icc_diff_left {α : Type u_1} [PartialOrder α] {a b : α} :
Icc a b \ {a} = Ioc a b
source
@[simp]
theorem Set.Icc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} :
Icc a b \ {b} = Ico a b
source
@[simp]
theorem Set.Ico_diff_left {α : Type u_1} [PartialOrder α] {a b : α} :
Ico a b \ {a} = Ioo a b
source
@[simp]
theorem Set.Ioc_diff_right {α : Type u_1} [PartialOrder α] {a b : α} :
Ioc a b \ {b} = Ioo a b
source
@[simp]
theorem Set.Icc_diff_both {α : Type u_1} [PartialOrder α] {a b : α} :
Icc a b \ {a, b} = Ioo a b
source
@[simp]
theorem Set.Ici_diff_left {α : Type u_1} [PartialOrder α] {a : α} :
Ici a \ {a} = Ioi a
source
@[simp]
theorem Set.Iic_diff_right {α : Type u_1} [PartialOrder α] {a : α} :
Iic a \ {a} = Iio a
source
@[simp]
theorem Set.Ico_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
Ico a b \ Ioo a b = {a}
source
@[simp]
theorem Set.Ioc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
Ioc a b \ Ioo a b = {b}
source
@[simp]
theorem Set.Icc_diff_Ico_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
Icc a b \ Ico a b = {b}
source
@[simp]
theorem Set.Icc_diff_Ioc_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
Icc a b \ Ioc a b = {a}
source
@[simp]
theorem Set.Icc_diff_Ioo_same {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
Icc a b \ Ioo a b = {a, b}
source
@[simp]
theorem Set.Ici_diff_Ioi_same {α : Type u_1} [PartialOrder α] {a : α} :
Ici a \ Ioi a = {a}
source
@[simp]
theorem Set.Iic_diff_Iio_same {α : Type u_1} [PartialOrder α] {a : α} :
Iic a \ Iio a = {a}
source
theorem Set.Ioi_union_left {α : Type u_1} [PartialOrder α] {a : α} :
Ioi a ∪ {a} = Ici a
source
theorem Set.Iio_union_right {α : Type u_1} [PartialOrder α] {a : α} :
Iio a ∪ {a} = Iic a
source
theorem Set.Ioo_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) :
Ioo a b ∪ {a} = Ico a b
source
theorem Set.Ioo_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a < b) :
Ioo a b ∪ {b} = Ioc a b
source
theorem Set.Ioo_union_both {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
Ioo a b ∪ {a, b} = Icc a b
source
theorem Set.Ioc_union_left {α : Type u_1} [PartialOrder α] {a b : α} (hab : a ≤ b) :
Ioc a b ∪ {a} = Icc a b
source
theorem Set.Ico_union_right {α : Type u_1} [PartialOrder α] {a b : α} (hab : a ≤ b) :
Ico a b ∪ {b} = Icc a b
source
@[simp]
theorem Set.Ico_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
insert b (Ico a b) = Icc a b
source
@[simp]
theorem Set.Ioc_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a ≤ b) :
insert a (Ioc a b) = Icc a b
source
@[simp]
theorem Set.Ioo_insert_left {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
insert a (Ioo a b) = Ico a b
source
@[simp]
theorem Set.Ioo_insert_right {α : Type u_1} [PartialOrder α] {a b : α} (h : a < b) :
insert b (Ioo a b) = Ioc a b
source
@[simp]
theorem Set.Iio_insert {α : Type u_1} [PartialOrder α] {a : α} :
insert a (Iio a) = Iic a
source
@[simp]
theorem Set.Ioi_insert {α : Type u_1} [PartialOrder α] {a : α} :
insert a (Ioi a) = Ici a
source
theorem Set.mem_Ici_Ioi_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
s ∈ {Ici a, Ioi a}
source
theorem Set.mem_Iic_Iio_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a : α} {s : Set α} (ho : Iio a ⊆ s) (hc : s ⊆ Iic a) :
s ∈ {Iic a, Iio a}
source
theorem Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {α : Type u_1} [PartialOrder α] {a b : α} {s : Set α} (ho : Ioo a b ⊆ s) (hc : s ⊆ Icc a b) :
s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
source
theorem Set.eq_left_or_mem_Ioo_of_mem_Ico {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Ico a b) :
x = a ∨ x ∈ Ioo a b
source
theorem Set.eq_right_or_mem_Ioo_of_mem_Ioc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Ioc a b) :
x = b ∨ x ∈ Ioo a b
source
theorem Set.eq_endpoints_or_mem_Ioo_of_mem_Icc {α : Type u_1} [PartialOrder α] {a b x : α} (hmem : x ∈ Icc a b) :
x = a ∨ x = b ∨ x ∈ Ioo a b
source
theorem IsMax.Ici_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMax a) :
Set.Ici a = {a}
source
theorem IsMin.Iic_eq {α : Type u_1} [PartialOrder α] {a : α} (h : IsMin a) :
Set.Iic a = {a}
source
theorem Set.Ici_injective {α : Type u_1} [PartialOrder α] :
Function.Injective Ici
source
theorem Set.Iic_injective {α : Type u_1} [PartialOrder α] :
Function.Injective Iic
source
theorem Set.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} :
Ici a = Ici b ↔ a = b
source
theorem Set.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} :
Iic a = Iic b ↔ a = b
source
@[simp]
theorem Set.Icc_inter_Icc_eq_singleton {α : Type u_1} [PartialOrder α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
Icc a b ∩ Icc b c = {b}
source
theorem Set.Icc_eq_Icc_iff {α : Type u_1} [PartialOrder α] {a b c d : α} (h : a ≤ b) :
Icc a b = Icc c d ↔ a = c ∧ b = d
source
@[simp]
theorem Set.Ici_top {α : Type u_1} [PartialOrder α] [OrderTop α] :
Ici ⊤ = {⊤}
source
theorem Set.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :
Ioi ⊤ = ∅
source
@[simp]
theorem Set.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :
Iic ⊤ = univ
source
@[simp]
theorem Set.Icc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
Icc a ⊤ = Ici a
source
@[simp]
theorem Set.Ioc_top {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
Ioc a ⊤ = Ioi a
source
@[simp]
theorem Set.Iic_bot {α : Type u_1} [PartialOrder α] [OrderBot α] :
Iic ⊥ = {⊥}
source
theorem Set.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :
Iio ⊥ = ∅
source
@[simp]
theorem Set.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :
Ici ⊥ = univ
source
@[simp]
theorem Set.Icc_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
Icc ⊥ a = Iic a
source
@[simp]
theorem Set.Ico_bot {α : Type u_1} [Preorder α] [OrderBot α] {a : α} :
Ico ⊥ a = Iio a
source
theorem Set.Icc_bot_top {α : Type u_1} [Preorder α] [BoundedOrder α] :
Icc ⊥ ⊤ = univ
source
@[simp]
theorem Set.Iic_inter_Iic {α : Type u_1} [SemilatticeInf α] {a b : α} :
Iic a ∩ Iic b = Iic (a ⊓ b)
source
@[simp]
theorem Set.Ioc_inter_Iic {α : Type u_1} [SemilatticeInf α] (a b c : α) :
Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
source
@[simp]
theorem Set.Ici_inter_Ici {α : Type u_1} [SemilatticeSup α] {a b : α} :
Ici a ∩ Ici b = Ici (a ⊔ b)
source
@[simp]
theorem Set.Ico_inter_Ici {α : Type u_1} [SemilatticeSup α] (a b c : α) :
Ico a b ∩ Ici c = Ico (a ⊔ c) b
source
theorem Set.Icc_inter_Icc {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} :
Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Closed intervals in α × β #

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

Lemmas about intervals in dense orders #

source
instance instNoMinOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
NoMinOrder ↑(Set.Ioo x y)
source
instance instNoMinOrderElemIoc (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
NoMinOrder ↑(Set.Ioc x y)
source
instance instNoMinOrderElemIoi (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :
NoMinOrder ↑(Set.Ioi x)
source
instance instNoMaxOrderElemIoo (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
NoMaxOrder ↑(Set.Ioo x y)
source
instance instNoMaxOrderElemIco (α : Type u_1) [Preorder α] [DenselyOrdered α] {x y : α} :
NoMaxOrder ↑(Set.Ico x y)
source
instance instNoMaxOrderElemIio (α : Type u_1) [Preorder α] [DenselyOrdered α] {x : α} :
NoMaxOrder ↑(Set.Iio x)

Intervals in Prop #

source
@[simp]
theorem Set.Iic_False :
Iic False = {False}
source
@[simp]
theorem Set.Iic_True :
Iic True = univ
source
@[simp]
theorem Set.Ici_False :
Ici False = univ
source
@[simp]
theorem Set.Ici_True :
Ici True = {True}
source
theorem Set.Iio_False :
Iio False = ∅
source
@[simp]
theorem Set.Iio_True :
Iio True = {False}
source
@[simp]
theorem Set.Ioi_False :
Ioi False = {True}
source
theorem Set.Ioi_True :
Ioi True = ∅