mathlib documentation

data.set.intervals.unordered_interval

Intervals without endpoints ordering

In any decidable linear order α, we define the set of elements lying between two elements a and b as Icc (min a b) (max a b).

Icc a b requires the assumption a ≤ b to be meaningful, which is sometimes inconvenient. The interval as defined in this file is always the set of things lying between a and b, regardless of the relative order of a and b.

For real numbers, Icc (min a b) (max a b) is the same as segment a b.

Notation

We use the localized notation [a, b] for interval a b. One can open the locale interval to make the notation available.

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

interval a b is the set of elements lying between a and b, with a and b included.

Equations
source
@[simp]
theorem set.interval_of_le {α : Type u} [decidable_linear_order α] {a b : α} (h : a ≤ b) :
set.interval a b = set.Icc a b

source
@[simp]
theorem set.interval_of_ge {α : Type u} [decidable_linear_order α] {a b : α} (h : b ≤ a) :
set.interval a b = set.Icc b a

source
theorem set.interval_swap {α : Type u} [decidable_linear_order α] (a b : α) :
set.interval a b = set.interval b a

source
theorem set.interval_of_lt {α : Type u} [decidable_linear_order α] {a b : α} (h : a < b) :
set.interval a b = set.Icc a b

source
theorem set.interval_of_gt {α : Type u} [decidable_linear_order α] {a b : α} (h : b < a) :
set.interval a b = set.Icc b a

source
theorem set.interval_of_not_le {α : Type u} [decidable_linear_order α] {a b : α} (h : ¬a ≤ b) :
set.interval a b = set.Icc b a

source
theorem set.interval_of_not_ge {α : Type u} [decidable_linear_order α] {a b : α} (h : ¬b ≤ a) :
set.interval a b = set.Icc a b

source
@[simp]
theorem set.interval_self {α : Type u} [decidable_linear_order α] {a : α} :
set.interval a a = {a}

source
@[simp]
theorem set.nonempty_interval {α : Type u} [decidable_linear_order α] {a b : α} :
(set.interval a b).nonempty

source
@[simp]
theorem set.left_mem_interval {α : Type u} [decidable_linear_order α] {a b : α} :
a ∈ set.interval a b

source
@[simp]
theorem set.right_mem_interval {α : Type u} [decidable_linear_order α] {a b : α} :
b ∈ set.interval a b

source
theorem set.Icc_subset_interval {α : Type u} [decidable_linear_order α] {a b : α} :
set.Icc a b ⊆ set.interval a b

source
theorem set.Icc_subset_interval' {α : Type u} [decidable_linear_order α] {a b : α} :
set.Icc b a ⊆ set.interval a b

source
theorem set.mem_interval_of_le {α : Type u} [decidable_linear_order α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) :
x ∈ set.interval a b

source
theorem set.mem_interval_of_ge {α : Type u} [decidable_linear_order α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) :
x ∈ set.interval a b

source
theorem set.interval_subset_interval {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ∈ set.interval a₂ b₂) (h₂ : b₁ ∈ set.interval a₂ b₂) :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂

source
theorem set.interval_subset_interval_iff_mem {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂ ↔ a₁ ∈ set.interval a₂ b₂ ∧ b₁ ∈ set.interval a₂ b₂

source
theorem set.interval_subset_interval_iff_le {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
set.interval a₁ b₁ ⊆ set.interval a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂

source
theorem set.interval_subset_interval_right {α : Type u} [decidable_linear_order α] {a b x : α} (h : x ∈ set.interval a b) :
set.interval x b ⊆ set.interval a b

source
theorem set.interval_subset_interval_left {α : Type u} [decidable_linear_order α] {a b x : α} (h : x ∈ set.interval a b) :
set.interval a x ⊆ set.interval a b

source
theorem set.bdd_below_bdd_above_iff_subset_interval {α : Type u} [decidable_linear_order α] (s : set α) :
bdd_below s ∧ bdd_above s ↔ ∃ (a b : α), s ⊆ set.interval a b

source
theorem set.abs_sub_le_of_subinterval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x y : α} (h : set.interval x y ⊆ set.interval a b) :
abs (y - x) ≤ abs (b - a)

If [x, y] is a subinterval of [a, b], then the distance between x and y is less than or equal to that of a and b

source
theorem set.abs_sub_left_of_mem_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x : α} (h : x ∈ set.interval a b) :
abs (x - a) ≤ abs (b - a)

If x ∈ [a, b], then the distance between a and x is less than or equal to that of a and b

source
theorem set.abs_sub_right_of_mem_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x : α} (h : x ∈ set.interval a b) :
abs (b - x) ≤ abs (b - a)

If x ∈ [a, b], then the distance between x and b is less than or equal to that of a and b