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 α] :

α → α → set α

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

Equations

set.interval a b = set.Icc (min a b) (max a b)

source

@[simp]

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

a ≤ b → set.interval a b = set.Icc a b

source

@[simp]

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

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 : α} :

a < b → set.interval a b = set.Icc a b

source

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

b < a → set.interval a b = set.Icc b a

source

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

¬a ≤ b → set.interval a b = set.Icc b a

source

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

¬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 : α} :

a ≤ x → x ≤ b → x ∈ set.interval a b

source

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

b ≤ x → x ≤ a → x ∈ set.interval a b

source

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₂

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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 : α} :

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

mathlib documentation

data.set.intervals.unordered_interval

Intervals without endpoints ordering

Notation

General documentation

Additional documentation

Library

mathlib documentation

data.​set.​intervals.​unordered_interval

Intervals without endpoints ordering

Notation

General documentation

Additional documentation

Library

data.set.intervals.unordered_interval