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_1} [linear_order α] (a b : α) :
set α

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

Equations
Instances for set.interval
@[simp]
theorem set.interval_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
@[simp]
theorem set.interval_of_ge {α : Type u_1} [linear_order α] {a b : α} (h : b a) :
theorem set.interval_swap {α : Type u_1} [linear_order α] (a b : α) :
theorem set.interval_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : a < b) :
theorem set.interval_of_gt {α : Type u_1} [linear_order α] {a b : α} (h : b < a) :
theorem set.interval_of_not_le {α : Type u_1} [linear_order α] {a b : α} (h : ¬a b) :
theorem set.interval_of_not_ge {α : Type u_1} [linear_order α] {a b : α} (h : ¬b a) :
theorem set.interval_eq_union {α : Type u_1} [linear_order α] {a b : α} :
theorem set.mem_interval {α : Type u_1} [linear_order α] {a b c : α} :
a set.interval b c b a a c c a a b
@[simp]
theorem set.interval_self {α : Type u_1} [linear_order α] {a : α} :
set.interval a a = {a}
@[simp]
theorem set.nonempty_interval {α : Type u_1} [linear_order α] {a b : α} :
@[simp]
theorem set.left_mem_interval {α : Type u_1} [linear_order α] {a b : α} :
@[simp]
theorem set.right_mem_interval {α : Type u_1} [linear_order α] {a b : α} :
theorem set.Icc_subset_interval {α : Type u_1} [linear_order α] {a b : α} :
theorem set.Icc_subset_interval' {α : Type u_1} [linear_order α] {a b : α} :
theorem set.mem_interval_of_le {α : Type u_1} [linear_order α] {a b x : α} (ha : a x) (hb : x b) :
theorem set.mem_interval_of_ge {α : Type u_1} [linear_order α] {a b x : α} (hb : b x) (ha : x a) :
theorem set.not_mem_interval_of_lt {α : Type u_1} [linear_order α] {a b c : α} (ha : c < a) (hb : c < b) :
theorem set.not_mem_interval_of_gt {α : Type u_1} [linear_order α] {a b c : α} (ha : a < c) (hb : b < c) :
theorem set.interval_subset_interval {α : Type u_1} [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₂
theorem set.interval_subset_Icc {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ set.Icc a₂ b₂) (hb : b₁ set.Icc a₂ b₂) :
set.interval a₁ b₁ set.Icc a₂ b₂
theorem set.interval_subset_interval_iff_mem {α : Type u_1} [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_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
set.interval a₁ b₁ set.interval a₂ b₂ linear_order.min a₂ b₂ linear_order.min a₁ b₁ linear_order.max a₁ b₁ linear_order.max a₂ b₂
theorem set.interval_subset_interval_right {α : Type u_1} [linear_order α] {a b x : α} (h : x set.interval a b) :
theorem set.interval_subset_interval_left {α : Type u_1} [linear_order α] {a b x : α} (h : x set.interval a b) :

A sort of triangle inequality.

theorem set.eq_of_mem_interval_of_mem_interval {α : Type u_1} [linear_order α] {a b c : α} :
theorem set.eq_of_mem_interval_of_mem_interval' {α : Type u_1} [linear_order α] {a b c : α} :
theorem set.interval_injective_right {α : Type u_1} [linear_order α] (a : α) :
function.injective (λ (b : α), set.interval b a)
theorem set.monotone_or_antitone_iff_interval {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α β} :
monotone f antitone f (a b c : α), c set.interval a b f c set.interval (f a) (f b)
theorem set.monotone_on_or_antitone_on_iff_interval {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α β} {s : set α} :
monotone_on f s antitone_on f s (a : α), a s (b : α), b s (c : α), c s c set.interval a b f c set.interval (f a) (f b)
def set.interval_oc {α : Type u_1} [linear_order α] :
α α set α

The open-closed interval with unordered bounds.

Equations
Instances for set.interval_oc
@[simp]
theorem set.interval_oc_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
@[simp]
theorem set.interval_oc_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : b < a) :
theorem set.interval_oc_eq_union {α : Type u_1} [linear_order α] {a b : α} :
theorem set.mem_interval_oc {α : Type u_1} [linear_order α] {a b c : α} :
a set.interval_oc b c b < a a c c < a a b
theorem set.not_mem_interval_oc {α : Type u_1} [linear_order α] {a b c : α} :
a set.interval_oc b c a b a c c < a b < a
@[simp]
theorem set.left_mem_interval_oc {α : Type u_1} [linear_order α] {a b : α} :
@[simp]
theorem set.right_mem_interval_oc {α : Type u_1} [linear_order α] {a b : α} :
theorem set.forall_interval_oc_iff {α : Type u_1} [linear_order α] {a b : α} {P : α Prop} :
( (x : α), x set.interval_oc a b P x) ( (x : α), x set.Ioc a b P x) (x : α), x set.Ioc b a P x
theorem set.interval_oc_swap {α : Type u_1} [linear_order α] (a b : α) :
theorem set.Ioc_subset_interval_oc {α : Type u_1} [linear_order α] {a b : α} :
theorem set.Ioc_subset_interval_oc' {α : Type u_1} [linear_order α] {a b : α} :
theorem set.eq_of_not_mem_interval_oc_of_not_mem_interval_oc {α : Type u_1} [linear_order α] {a b c : α} (ha : a c) (hb : b c) :
theorem set.interval_oc_injective_right {α : Type u_1} [linear_order α] (a : α) :