# mathlib3documentation

data.set.intervals.unordered_interval

# Intervals without endpoints ordering #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In any lattice α, we define uIcc a b to be Icc (a ⊓ b) (a ⊔ b), which in a linear order is the set of elements lying between a and 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, uIcc a b is the same as segment ℝ a b.

In a product or pi type, uIcc a b is the smallest box containing a and b. For example, uIcc (1, -1) (-1, 1) = Icc (-1, -1) (1, 1) is the square of vertices (1, -1), (-1, -1), (-1, 1), (1, 1).

In finset α (seen as a hypercube of dimension fintype.card α), uIcc a b is the smallest subcube containing both a and b.

## Notation #

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

def set.uIcc {α : Type u_1} [lattice α] (a b : α) :
set α

uIcc a b is the set of elements lying between a and b, with a and b included. Note that we define it more generally in a lattice as set.Icc (a ⊓ b) (a ⊔ b). In a product type, uIcc corresponds to the bounding box of the two elements.

Equations
Instances for set.uIcc
Instances for ↥set.uIcc
@[simp]
theorem set.dual_uIcc {α : Type u_1} [lattice α] (a b : α) :
@[simp]
theorem set.uIcc_of_le {α : Type u_1} [lattice α] {a b : α} (h : a b) :
b = b
@[simp]
theorem set.uIcc_of_ge {α : Type u_1} [lattice α] {a b : α} (h : b a) :
b = a
theorem set.uIcc_comm {α : Type u_1} [lattice α] (a b : α) :
b = a
theorem set.uIcc_of_lt {α : Type u_1} [lattice α] {a b : α} (h : a < b) :
b = b
theorem set.uIcc_of_gt {α : Type u_1} [lattice α] {a b : α} (h : b < a) :
b = a
@[simp]
theorem set.uIcc_self {α : Type u_1} [lattice α] {a : α} :
a = {a}
@[simp]
theorem set.nonempty_uIcc {α : Type u_1} [lattice α] {a b : α} :
theorem set.Icc_subset_uIcc {α : Type u_1} [lattice α] {a b : α} :
b b
theorem set.Icc_subset_uIcc' {α : Type u_1} [lattice α] {a b : α} :
a b
@[simp]
theorem set.left_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :
a b
@[simp]
theorem set.right_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :
b b
theorem set.mem_uIcc_of_le {α : Type u_1} [lattice α] {a b x : α} (ha : a x) (hb : x b) :
x b
theorem set.mem_uIcc_of_ge {α : Type u_1} [lattice α] {a b x : α} (hb : b x) (ha : x a) :
x b
theorem set.uIcc_subset_uIcc {α : Type u_1} [lattice α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ set.uIcc a₂ b₂) (h₂ : b₁ set.uIcc a₂ b₂) :
set.uIcc a₁ b₁ set.uIcc a₂ b₂
theorem set.uIcc_subset_Icc {α : Type u_1} [lattice α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ set.Icc a₂ b₂) (hb : b₁ set.Icc a₂ b₂) :
set.uIcc a₁ b₁ set.Icc a₂ b₂
theorem set.uIcc_subset_uIcc_iff_mem {α : Type u_1} [lattice α] {a₁ a₂ b₁ b₂ : α} :
set.uIcc a₁ b₁ set.uIcc a₂ b₂ a₁ set.uIcc a₂ b₂ b₁ set.uIcc a₂ b₂
theorem set.uIcc_subset_uIcc_iff_le' {α : Type u_1} [lattice α] {a₁ a₂ b₁ b₂ : α} :
set.uIcc a₁ b₁ set.uIcc a₂ b₂ a₂ b₂ a₁ b₁ a₁ b₁ a₂ b₂
theorem set.uIcc_subset_uIcc_right {α : Type u_1} [lattice α] {a b x : α} (h : x b) :
b b
theorem set.uIcc_subset_uIcc_left {α : Type u_1} [lattice α] {a b x : α} (h : x b) :
x b
theorem set.bdd_below_bdd_above_iff_subset_uIcc {α : Type u_1} [lattice α] (s : set α) :
(a b : α), s b
@[simp]
theorem set.uIcc_prod_uIcc {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] (a₁ a₂ : α) (b₁ b₂ : β) :
set.uIcc a₁ a₂ ×ˢ set.uIcc b₁ b₂ = set.uIcc (a₁, b₁) (a₂, b₂)
theorem set.uIcc_prod_eq {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] (a b : α × β) :
b = b.fst ×ˢ b.snd
theorem set.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} {a b c : α} (ha : a c) (hb : b c) :
a = b
theorem set.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_1} {a b c : α} :
b c c b b = c
theorem set.uIcc_injective_right {α : Type u_1} (a : α) :
function.injective (λ (b : α), a)
theorem set.uIcc_injective_left {α : Type u_1} (a : α) :
theorem monotone_on.image_uIcc_subset {α : Type u_1} {β : Type u_2} [linear_order α] [lattice β] {f : α β} {a b : α} (hf : (set.uIcc a b)) :
f '' b set.uIcc (f a) (f b)
theorem antitone_on.image_uIcc_subset {α : Type u_1} {β : Type u_2} [linear_order α] [lattice β] {f : α β} {a b : α} (hf : (set.uIcc a b)) :
f '' b set.uIcc (f a) (f b)
theorem monotone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [linear_order α] [lattice β] {f : α β} {a b : α} (hf : monotone f) :
f '' b set.uIcc (f a) (f b)
theorem antitone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [linear_order α] [lattice β] {f : α β} {a b : α} (hf : antitone f) :
f '' b set.uIcc (f a) (f b)
theorem set.Icc_min_max {α : Type u_1} [linear_order α] {a b : α} :
set.Icc b) b) = b
theorem set.uIcc_of_not_le {α : Type u_1} [linear_order α] {a b : α} (h : ¬a b) :
b = a
theorem set.uIcc_of_not_ge {α : Type u_1} [linear_order α] {a b : α} (h : ¬b a) :
b = b
theorem set.uIcc_eq_union {α : Type u_1} [linear_order α] {a b : α} :
b = b a
theorem set.mem_uIcc {α : Type u_1} [linear_order α] {a b c : α} :
a c b a a c c a a b
theorem set.not_mem_uIcc_of_lt {α : Type u_1} [linear_order α] {a b c : α} (ha : c < a) (hb : c < b) :
c b
theorem set.not_mem_uIcc_of_gt {α : Type u_1} [linear_order α] {a b c : α} (ha : a < c) (hb : b < c) :
c b
theorem set.uIcc_subset_uIcc_iff_le {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
set.uIcc a₁ b₁ set.uIcc a₂ b₂ b₂ b₁ b₁ b₂
theorem set.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [linear_order α] {a b c : α} :
c b c

A sort of triangle inequality.

theorem set.monotone_or_antitone_iff_uIcc {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α β} :
(a b c : α), c b f c set.uIcc (f a) (f b)
theorem set.monotone_on_or_antitone_on_iff_uIcc {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] {f : α β} {s : set α} :
s s (a : α), a s (b : α), b s (c : α), c s c b f c set.uIcc (f a) (f b)
def set.uIoc {α : Type u_1} [linear_order α] :
α α set α

The open-closed interval with unordered bounds.

Equations
Instances for set.uIoc
@[simp]
theorem set.uIoc_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
b = b
@[simp]
theorem set.uIoc_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : b < a) :
b = a
theorem set.uIoc_eq_union {α : Type u_1} [linear_order α] {a b : α} :
b = b a
theorem set.mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a c b < a a c c < a a b
theorem set.not_mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a c a b a c c < a b < a
@[simp]
theorem set.left_mem_uIoc {α : Type u_1} [linear_order α] {a b : α} :
a b b < a
@[simp]
theorem set.right_mem_uIoc {α : Type u_1} [linear_order α] {a b : α} :
b b a < b
theorem set.forall_uIoc_iff {α : Type u_1} [linear_order α] {a b : α} {P : α Prop} :
( (x : α), x b P x) ( (x : α), x b P x) (x : α), x a P x
theorem set.uIoc_subset_uIoc_of_uIcc_subset_uIcc {α : Type u_1} [linear_order α] {a b c d : α} (h : b d) :
b d
theorem set.uIoc_swap {α : Type u_1} [linear_order α] (a b : α) :
b = a
theorem set.Ioc_subset_uIoc {α : Type u_1} [linear_order α] {a b : α} :
b b
theorem set.Ioc_subset_uIoc' {α : Type u_1} [linear_order α] {a b : α} :
b a
theorem set.eq_of_mem_uIoc_of_mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a c b c a = b
theorem set.eq_of_mem_uIoc_of_mem_uIoc' {α : Type u_1} [linear_order α] {a b c : α} :
b c c b b = c
theorem set.eq_of_not_mem_uIoc_of_not_mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} (ha : a c) (hb : b c) :
a c b c a = b
theorem set.uIoc_injective_right {α : Type u_1} [linear_order α] (a : α) :
function.injective (λ (b : α), a)
theorem set.uIoc_injective_left {α : Type u_1} [linear_order α] (a : α) :