# Intervals without endpoints ordering #

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} [] (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

[[a, b]] denotes the set of elements lying between a and b, inclusive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Set.dual_uIcc {α : Type u_1} [] (a : α) (b : α) :
Set.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = OrderDual.ofDual ⁻¹' Set.uIcc a b
@[simp]
theorem Set.uIcc_of_le {α : Type u_1} [] {a : α} {b : α} (h : a b) :
@[simp]
theorem Set.uIcc_of_ge {α : Type u_1} [] {a : α} {b : α} (h : b a) :
theorem Set.uIcc_comm {α : Type u_1} [] (a : α) (b : α) :
theorem Set.uIcc_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
theorem Set.uIcc_of_gt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
theorem Set.uIcc_self {α : Type u_1} [] {a : α} :
Set.uIcc a a = {a}
@[simp]
theorem Set.nonempty_uIcc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.Icc_subset_uIcc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.Icc_subset_uIcc' {α : Type u_1} [] {a : α} {b : α} :
@[simp]
theorem Set.left_mem_uIcc {α : Type u_1} [] {a : α} {b : α} :
@[simp]
theorem Set.right_mem_uIcc {α : Type u_1} [] {a : α} {b : α} :
theorem Set.mem_uIcc_of_le {α : Type u_1} [] {a : α} {b : α} {x : α} (ha : a x) (hb : x b) :
theorem Set.mem_uIcc_of_ge {α : Type u_1} [] {a : α} {b : α} {x : α} (hb : b x) (ha : x a) :
theorem Set.uIcc_subset_uIcc {α : Type u_1} [] {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} [] {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} [] {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} [] {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} [] {a : α} {b : α} {x : α} (h : x Set.uIcc a b) :
theorem Set.uIcc_subset_uIcc_left {α : Type u_1} [] {a : α} {b : α} {x : α} (h : x Set.uIcc a b) :
theorem Set.bdd_below_bdd_above_iff_subset_uIcc {α : Type u_1} [] (s : Set α) :
∃ (a : α) (b : α), s Set.uIcc a b
@[simp]
theorem Set.uIcc_prod_uIcc {α : Type u_1} {β : Type u_2} [] [] (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} [] [] (a : α × β) (b : α × β) :
Set.uIcc a b = Set.uIcc a.1 b.1 ×ˢ Set.uIcc a.2 b.2
theorem Set.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : a Set.uIcc b c) (hb : b Set.uIcc a c) :
a = b
theorem Set.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_1} [] {a : α} {b : α} {c : α} :
b Set.uIcc a cc Set.uIcc a bb = c
theorem Set.uIcc_injective_right {α : Type u_1} [] (a : α) :
Function.Injective fun (b : α) => Set.uIcc b a
theorem Set.uIcc_injective_left {α : Type u_1} [] (a : α) :
theorem MonotoneOn.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : MonotoneOn f (Set.uIcc a b)) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
theorem AntitoneOn.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : AntitoneOn f (Set.uIcc a b)) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
theorem Monotone.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
theorem Antitone.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
theorem MonotoneOn.image_uIcc_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : MonotoneOn f (Set.uIcc a b)) :
f '' Set.uIcc a b Set.uIcc (f a) (f b)
theorem AntitoneOn.image_uIcc_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : AntitoneOn f (Set.uIcc a b)) :
f '' Set.uIcc a b Set.uIcc (f a) (f b)
theorem Monotone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f '' Set.uIcc a b Set.uIcc (f a) (f b)
theorem Antitone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f '' Set.uIcc a b Set.uIcc (f a) (f b)
theorem Set.Icc_min_max {α : Type u_1} [] {a : α} {b : α} :
Set.Icc (min a b) (max a b) = Set.uIcc a b
theorem Set.uIcc_of_not_le {α : Type u_1} [] {a : α} {b : α} (h : ¬a b) :
theorem Set.uIcc_of_not_ge {α : Type u_1} [] {a : α} {b : α} (h : ¬b a) :
theorem Set.uIcc_eq_union {α : Type u_1} [] {a : α} {b : α} :
theorem Set.mem_uIcc {α : Type u_1} [] {a : α} {b : α} {c : α} :
a Set.uIcc b c b a a c c a a b
theorem Set.not_mem_uIcc_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : c < a) (hb : c < b) :
cSet.uIcc a b
theorem Set.not_mem_uIcc_of_gt {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : a < c) (hb : b < c) :
cSet.uIcc a b
theorem Set.uIcc_subset_uIcc_iff_le {α : Type u_1} [] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Set.uIcc a₁ b₁ Set.uIcc a₂ b₂ min a₂ b₂ min a₁ b₁ max a₁ b₁ max a₂ b₂
theorem Set.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [] {a : α} {b : α} {c : α} :

A sort of triangle inequality.

theorem Set.monotone_or_antitone_iff_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
∀ (a b c : α), c Set.uIcc a bf c Set.uIcc (f a) (f b)
theorem Set.monotoneOn_or_antitoneOn_iff_uIcc {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
as, bs, cs, c Set.uIcc a bf c Set.uIcc (f a) (f b)
def Set.uIoc {α : Type u_1} [] :
ααSet α

The open-closed uIcc with unordered bounds.

Equations
Instances For

Ι a b denotes the open-closed interval with unordered bounds. Here, Ι is a capital iota, distinguished from a capital i.

Equations
Instances For
@[simp]
theorem Set.uIoc_of_le {α : Type u_1} [] {a : α} {b : α} (h : a b) :
Ι a b = Set.Ioc a b
@[simp]
theorem Set.uIoc_of_lt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
Ι a b = Set.Ioc b a
theorem Set.uIoc_eq_union {α : Type u_1} [] {a : α} {b : α} :
Ι a b = Set.Ioc a b Set.Ioc b a
theorem Set.mem_uIoc {α : Type u_1} [] {a : α} {b : α} {c : α} :
a Ι b c b < a a c c < a a b
theorem Set.not_mem_uIoc {α : Type u_1} [] {a : α} {b : α} {c : α} :
aΙ b c a b a c c < a b < a
@[simp]
theorem Set.left_mem_uIoc {α : Type u_1} [] {a : α} {b : α} :
a Ι a b b < a
@[simp]
theorem Set.right_mem_uIoc {α : Type u_1} [] {a : α} {b : α} :
b Ι a b a < b
theorem Set.forall_uIoc_iff {α : Type u_1} [] {a : α} {b : α} {P : αProp} :
(xΙ a b, P x) (xSet.Ioc a b, P x) xSet.Ioc b a, P x
theorem Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc {α : Type u_1} [] {a : α} {b : α} {c : α} {d : α} (h : Set.uIcc a b Set.uIcc c d) :
Ι a b Ι c d
theorem Set.uIoc_comm {α : Type u_1} [] (a : α) (b : α) :
Ι a b = Ι b a
theorem Set.Ioc_subset_uIoc {α : Type u_1} [] {a : α} {b : α} :
Set.Ioc a b Ι a b
theorem Set.Ioc_subset_uIoc' {α : Type u_1} [] {a : α} {b : α} :
Set.Ioc a b Ι b a
theorem Set.eq_of_mem_uIoc_of_mem_uIoc {α : Type u_1} [] {a : α} {b : α} {c : α} :
a Ι b cb Ι a ca = b
theorem Set.eq_of_mem_uIoc_of_mem_uIoc' {α : Type u_1} [] {a : α} {b : α} {c : α} :
b Ι a cc Ι a bb = c
theorem Set.eq_of_not_mem_uIoc_of_not_mem_uIoc {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : a c) (hb : b c) :
aΙ b cbΙ a ca = b
theorem Set.uIoc_injective_right {α : Type u_1} [] (a : α) :
Function.Injective fun (b : α) => Ι b a
theorem Set.uIoc_injective_left {α : Type u_1} [] (a : α) :