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.

def set.interval {α : Type u} [decidable_linear_order α] :
α → α → set α

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

Equations
@[simp]
theorem set.interval_of_le {α : Type u} [decidable_linear_order α] {a b : α} :
a bset.interval a b = set.Icc a b

@[simp]
theorem set.interval_of_ge {α : Type u} [decidable_linear_order α] {a b : α} :
b aset.interval a b = set.Icc b a

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

theorem set.interval_of_lt {α : Type u} [decidable_linear_order α] {a b : α} :
a < bset.interval a b = set.Icc a b

theorem set.interval_of_gt {α : Type u} [decidable_linear_order α] {a b : α} :
b < aset.interval a b = set.Icc b a

theorem set.interval_of_not_le {α : Type u} [decidable_linear_order α] {a b : α} :
¬a bset.interval a b = set.Icc b a

theorem set.interval_of_not_ge {α : Type u} [decidable_linear_order α] {a b : α} :
¬b aset.interval a b = set.Icc a b

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

@[simp]
theorem set.nonempty_interval {α : Type u} [decidable_linear_order α] {a b : α} :

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

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

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

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

theorem set.mem_interval_of_le {α : Type u} [decidable_linear_order α] {a b x : α} :
a xx bx set.interval a b

theorem set.mem_interval_of_ge {α : Type u} [decidable_linear_order α] {a b x : α} :
b xx ax set.interval a b

theorem set.interval_subset_interval {α : Type u} [decidable_linear_order α] {a₁ a₂ b₁ b₂ : α} :
a₁ set.interval a₂ b₂b₁ set.interval a₂ b₂set.interval a₁ b₁ set.interval a₂ b₂

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₂

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₂

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

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

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

@[simp]
theorem set.preimage_const_add_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) ⁻¹' set.interval b c = set.interval (b - a) (c - a)

@[simp]
theorem set.preimage_add_const_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) ⁻¹' set.interval b c = set.interval (b - a) (c - a)

@[simp]

@[simp]
theorem set.preimage_sub_const_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) ⁻¹' set.interval b c = set.interval (b + a) (c + a)

@[simp]
theorem set.preimage_const_sub_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) ⁻¹' set.interval b c = set.interval (a - b) (a - c)

@[simp]
theorem set.image_const_add_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) '' set.interval b c = set.interval (a + b) (a + c)

@[simp]
theorem set.image_add_const_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) '' set.interval b c = set.interval (b + a) (c + a)

@[simp]
theorem set.image_const_sub_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) '' set.interval b c = set.interval (a - b) (a - c)

@[simp]
theorem set.image_sub_const_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) '' set.interval b c = set.interval (b - a) (c - a)

theorem set.abs_sub_le_of_subinterval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x y : α} :
set.interval x y set.interval a babs (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

theorem set.abs_sub_left_of_mem_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x : α} :
x set.interval a babs (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

theorem set.abs_sub_right_of_mem_interval {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b x : α} :
x set.interval a babs (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

@[simp]
theorem set.preimage_mul_const_interval {k : Type u} [discrete_linear_ordered_field k] {a : k} (ha : a 0) (b c : k) :
(λ (x : k), x * a) ⁻¹' set.interval b c = set.interval (b / a) (c / a)

@[simp]
theorem set.preimage_const_mul_interval {k : Type u} [discrete_linear_ordered_field k] {a : k} (ha : a 0) (b c : k) :
(λ (x : k), a * x) ⁻¹' set.interval b c = set.interval (b / a) (c / a)

@[simp]
theorem set.preimage_div_const_interval {k : Type u} [discrete_linear_ordered_field k] {a : k} (ha : a 0) (b c : k) :
(λ (x : k), x / a) ⁻¹' set.interval b c = set.interval (b * a) (c * a)

@[simp]
theorem set.image_mul_const_interval {k : Type u} [discrete_linear_ordered_field k] (a b c : k) :
(λ (x : k), x * a) '' set.interval b c = set.interval (b * a) (c * a)

@[simp]
theorem set.image_const_mul_interval {k : Type u} [discrete_linear_ordered_field k] (a b c : k) :
(λ (x : k), a * x) '' set.interval b c = set.interval (a * b) (a * c)

@[simp]
theorem set.image_div_const_interval {k : Type u} [discrete_linear_ordered_field k] (a b c : k) :
(λ (x : k), x / a) '' set.interval b c = set.interval (b / a) (c / a)