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} [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} [linear_order α] {a b : α} (h : a ≤ b) :
[a, b] = set.Icc a b
source
@[simp]
theorem set.interval_of_ge {α : Type u} [linear_order α] {a b : α} (h : b ≤ a) :
[a, b] = set.Icc b a
source
theorem set.interval_swap {α : Type u} [linear_order α] (a b : α) :
[a, b] = [b, a]
source
theorem set.interval_of_lt {α : Type u} [linear_order α] {a b : α} (h : a < b) :
[a, b] = set.Icc a b
source
theorem set.interval_of_gt {α : Type u} [linear_order α] {a b : α} (h : b < a) :
[a, b] = set.Icc b a
source
theorem set.interval_of_not_le {α : Type u} [linear_order α] {a b : α} (h : ¬a ≤ b) :
[a, b] = set.Icc b a
source
theorem set.interval_of_not_ge {α : Type u} [linear_order α] {a b : α} (h : ¬b ≤ a) :
[a, b] = set.Icc a b
source
@[simp]
theorem set.interval_self {α : Type u} [linear_order α] {a : α} :
[a, a] = {a}
source
@[simp]
theorem set.nonempty_interval {α : Type u} [linear_order α] {a b : α} :
[a, b].nonempty
source
@[simp]
theorem set.left_mem_interval {α : Type u} [linear_order α] {a b : α} :
a ∈ [a, b]
source
@[simp]
theorem set.right_mem_interval {α : Type u} [linear_order α] {a b : α} :
b ∈ [a, b]
source
theorem set.Icc_subset_interval {α : Type u} [linear_order α] {a b : α} :
set.Icc a b ⊆ [a, b]
source
theorem set.Icc_subset_interval' {α : Type u} [linear_order α] {a b : α} :
set.Icc b a ⊆ [a, b]
source
theorem set.mem_interval_of_le {α : Type u} [linear_order α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) :
x ∈ [a, b]
source
theorem set.mem_interval_of_ge {α : Type u} [linear_order α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) :
x ∈ [a, b]
source
theorem set.not_mem_interval_of_lt {α : Type u} [linear_order α] {a b c : α} (ha : c < a) (hb : c < b) :
c ∉ [a, b]
source
theorem set.not_mem_interval_of_gt {α : Type u} [linear_order α] {a b c : α} (ha : a < c) (hb : b < c) :
c ∉ [a, b]
source
theorem set.interval_subset_interval {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ∈ [a₂, b₂]) (h₂ : b₁ ∈ [a₂, b₂]) :
[a₁, b₁] ⊆ [a₂, b₂]
source
theorem set.interval_subset_Icc {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ set.Icc a₂ b₂) (hb : b₁ ∈ set.Icc a₂ b₂) :
[a₁, b₁] ⊆ set.Icc a₂ b₂
source
theorem set.interval_subset_interval_iff_mem {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
[a₁, b₁] ⊆ [a₂, b₂] ↔ a₁ ∈ [a₂, b₂] ∧ b₁ ∈ [a₂, b₂]
source
theorem set.interval_subset_interval_iff_le {α : Type u} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
[a₁, b₁] ⊆ [a₂, b₂] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
source
theorem set.interval_subset_interval_right {α : Type u} [linear_order α] {a b x : α} (h : x ∈ [a, b]) :
[x, b] ⊆ [a, b]
source
theorem set.interval_subset_interval_left {α : Type u} [linear_order α] {a b x : α} (h : x ∈ [a, b]) :
[a, x] ⊆ [a, b]
source
theorem set.interval_subset_interval_union_interval {α : Type u} [linear_order α] {a b c : α} :
[a, c] ⊆ [a, b] ∪ [b, c]

A sort of triangle inequality.

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

The open-closed interval with unordered bounds.

Equations
source
theorem set.interval_oc_of_le {α : Type u} [linear_order α] {a b : α} (h : a ≤ b) :
Ι a b = set.Ioc a b
source
theorem set.interval_oc_of_lt {α : Type u} [linear_order α] {a b : α} (h : b < a) :
Ι a b = set.Ioc b a
source
theorem set.interval_oc_eq_union {α : Type u} [linear_order α] {a b : α} :
Ι a b = set.Ioc a b ∪ set.Ioc b a
source
theorem set.forall_interval_oc_iff {α : Type u} [linear_order α] {a b : α} {P : α → Prop} :
(∀ (x : α), x ∈ Ι a b → P x) ↔ (∀ (x : α), x ∈ set.Ioc a b → P x) ∧ ∀ (x : α), x ∈ set.Ioc b a → P x
source
theorem set.interval_oc_subset_interval_oc_of_interval_subset_interval {α : Type u} [linear_order α] {a b c d : α} (h : [a, b] ⊆ [c, d]) :
Ι a b ⊆ Ι c d
source
theorem set.interval_oc_swap {α : Type u} [linear_order α] (a b : α) :
Ι a b = Ι b a
source
@[simp]
theorem set.preimage_const_add_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) ⁻¹' [b, c] = [b - a, c - a]
source
@[simp]
theorem set.preimage_add_const_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) ⁻¹' [b, c] = [b - a, c - a]
source
@[simp]
theorem set.preimage_neg_interval {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
-[a, b] = [-a, -b]
source
@[simp]
theorem set.preimage_sub_const_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) ⁻¹' [b, c] = [b + a, c + a]
source
@[simp]
theorem set.preimage_const_sub_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) ⁻¹' [b, c] = [a - b, a - c]
source
@[simp]
theorem set.image_const_add_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) '' [b, c] = [a + b, a + c]
source
@[simp]
theorem set.image_add_const_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) '' [b, c] = [b + a, c + a]
source
@[simp]
theorem set.image_const_sub_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) '' [b, c] = [a - b, a - c]
source
@[simp]
theorem set.image_sub_const_interval {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) '' [b, c] = [b - a, c - a]
source
theorem set.image_neg_interval {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
has_neg.neg '' [a, b] = [-a, -b]
source
theorem set.abs_sub_le_of_subinterval {α : Type u} [linear_ordered_add_comm_group α] {a b x y : α} (h : [x, y] ⊆ [a, b]) :
|y - x| ≤ |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} [linear_ordered_add_comm_group α] {a b x : α} (h : x ∈ [a, b]) :
|x - a| ≤ |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} [linear_ordered_add_comm_group α] {a b x : α} (h : x ∈ [a, b]) :
|b - x| ≤ |b - a|

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

source
@[simp]
theorem set.preimage_mul_const_interval {k : Type u} [linear_ordered_field k] {a : k} (ha : a ≠ 0) (b c : k) :
(λ (x : k), x * a) ⁻¹' [b, c] = [b / a, c / a]
source
@[simp]
theorem set.preimage_const_mul_interval {k : Type u} [linear_ordered_field k] {a : k} (ha : a ≠ 0) (b c : k) :
(λ (x : k), a * x) ⁻¹' [b, c] = [b / a, c / a]
source
@[simp]
theorem set.preimage_div_const_interval {k : Type u} [linear_ordered_field k] {a : k} (ha : a ≠ 0) (b c : k) :
(λ (x : k), x / a) ⁻¹' [b, c] = [b * a, c * a]
source
@[simp]
theorem set.image_mul_const_interval {k : Type u} [linear_ordered_field k] (a b c : k) :
(λ (x : k), x * a) '' [b, c] = [b * a, c * a]
source
@[simp]
theorem set.image_const_mul_interval {k : Type u} [linear_ordered_field k] (a b c : k) :
(λ (x : k), a * x) '' [b, c] = [a * b, a * c]
source
@[simp]
theorem set.image_div_const_interval {k : Type u} [linear_ordered_field k] (a b c : k) :
(λ (x : k), x / a) '' [b, c] = [b / a, c / a]