# 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 scope `Interval` to make the notation available.

source
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

- Set.uIcc a b = Set.Icc (a ⊓ b) (a ⊔ b)

Instances For

source
def Interval.«term[[_,_]]» :
Lean.ParserDescr

`[[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

source
@[simp]
theorem Set.uIcc_toDual {α : Type u_1} [Lattice α] (a b : α) :
uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIcc a b
source
@[simp]
theorem Set.uIcc_ofDual {α : Type u_1} [Lattice α] (a b : α ᵒᵈ) :
uIcc (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' uIcc a b
source
@[simp]
theorem Set.uIcc_of_le {α : Type u_1} [Lattice α] {a b : α} (h : a ≤ b) :
uIcc a b = Icc a b
source
@[simp]
theorem Set.uIcc_of_ge {α : Type u_1} [Lattice α] {a b : α} (h : b ≤ a) :
uIcc a b = Icc b a
source
theorem Set.uIcc_comm {α : Type u_1} [Lattice α] (a b : α) :
uIcc a b = uIcc b a
source
theorem Set.uIcc_of_lt {α : Type u_1} [Lattice α] {a b : α} (h : a < b) :
uIcc a b = Icc a b
source
theorem Set.uIcc_of_gt {α : Type u_1} [Lattice α] {a b : α} (h : b < a) :
uIcc a b = Icc b a
source
theorem Set.uIcc_self {α : Type u_1} [Lattice α] {a : α} :
uIcc a a = {a}
source
@[simp]
theorem Set.nonempty_uIcc {α : Type u_1} [Lattice α] {a b : α} :
(uIcc a b).Nonempty
source
theorem Set.Icc_subset_uIcc {α : Type u_1} [Lattice α] {a b : α} :
Icc a b ⊆ uIcc a b
source
theorem Set.Icc_subset_uIcc' {α : Type u_1} [Lattice α] {a b : α} :
Icc b a ⊆ uIcc a b
source
@[simp]
theorem Set.left_mem_uIcc {α : Type u_1} [Lattice α] {a b : α} :
a ∈ uIcc a b
source
@[simp]
theorem Set.right_mem_uIcc {α : Type u_1} [Lattice α] {a b : α} :
b ∈ uIcc a b
source
theorem Set.mem_uIcc_of_le {α : Type u_1} [Lattice α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) :
x ∈ uIcc a b
source
theorem Set.mem_uIcc_of_ge {α : Type u_1} [Lattice α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) :
x ∈ uIcc a b
source
theorem Set.uIcc_subset_uIcc {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ∈ uIcc a₂ b₂) (h₂ : b₁ ∈ uIcc a₂ b₂) :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂
source
theorem Set.uIcc_subset_Icc {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) :
uIcc a₁ b₁ ⊆ Icc a₂ b₂
source
theorem Set.uIcc_subset_uIcc_iff_mem {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ a₁ ∈ uIcc a₂ b₂ ∧ b₁ ∈ uIcc a₂ b₂
source
theorem Set.uIcc_subset_uIcc_iff_le' {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
source
theorem Set.uIcc_subset_uIcc_right {α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ uIcc a b) :
uIcc x b ⊆ uIcc a b
source
theorem Set.uIcc_subset_uIcc_left {α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ uIcc a b) :
uIcc a x ⊆ uIcc a b
source
theorem Set.bdd_below_bdd_above_iff_subset_uIcc {α : Type u_1} [Lattice α] (s : Set α) :
BddBelow s ∧ BddAbove s ↔ ∃ (a : α) (b : α), s ⊆ uIcc a b
source
@[simp]
theorem Set.uIcc_prod_uIcc {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a₁ a₂ : α) (b₁ b₂ : β) :
uIcc a₁ a₂ ×ˢ uIcc b₁ b₂ = uIcc (a₁, b₁) (a₂, b₂)
source
theorem Set.uIcc_prod_eq {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a b : α × β) :
uIcc a b = uIcc a.1 b.1 ×ˢ uIcc a.2 b.2
source
theorem Set.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [DistribLattice α] {a b c : α} (ha : a ∈ uIcc b c) (hb : b ∈ uIcc a c) :
a = b
source
theorem Set.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_1} [DistribLattice α] {a b c : α} :
b ∈ uIcc a c → c ∈ uIcc a b → b = c
source
theorem Set.uIcc_injective_right {α : Type u_1} [DistribLattice α] (a : α) :
Function.Injective fun (b : α) => uIcc b a
source
theorem Set.uIcc_injective_left {α : Type u_1} [DistribLattice α] (a : α) :
Function.Injective (uIcc a)
source
theorem MonotoneOn.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
source
theorem AntitoneOn.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
source
theorem Monotone.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Monotone f) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
source
theorem Antitone.mapsTo_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Antitone f) :
Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
source
theorem MonotoneOn.image_uIcc_subset {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) :
f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
source
theorem AntitoneOn.image_uIcc_subset {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) :
f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
source
theorem Monotone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Monotone f) :
f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
source
theorem Antitone.image_uIcc_subset {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Antitone f) :
f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
source
theorem Set.Icc_min_max {α : Type u_1} [LinearOrder α] {a b : α} :
Icc (min a b) (max a b) = uIcc a b
source
theorem Set.uIcc_of_not_le {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a ≤ b) :
uIcc a b = Icc b a
source
theorem Set.uIcc_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) :
uIcc a b = Icc a b
source
theorem Set.uIcc_eq_union {α : Type u_1} [LinearOrder α] {a b : α} :
uIcc a b = Icc a b ∪ Icc b a
source
theorem Set.mem_uIcc {α : Type u_1} [LinearOrder α] {a b c : α} :
a ∈ uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
source
theorem Set.notMem_uIcc_of_lt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : c < a) (hb : c < b) :
c ∉ uIcc a b
source
@[deprecated Set.notMem_uIcc_of_lt (since := "2025-05-23")]
theorem Set.not_mem_uIcc_of_lt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : c < a) (hb : c < b) :
c ∉ uIcc a b

Alias of `Set.notMem_uIcc_of_lt`.

source
theorem Set.notMem_uIcc_of_gt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a < c) (hb : b < c) :
c ∉ uIcc a b
source
@[deprecated Set.notMem_uIcc_of_gt (since := "2025-05-23")]
theorem Set.not_mem_uIcc_of_gt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a < c) (hb : b < c) :
c ∉ uIcc a b

Alias of `Set.notMem_uIcc_of_gt`.

source
theorem Set.uIcc_subset_uIcc_iff_le {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
source
theorem Set.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [LinearOrder α] {a b c : α} :
uIcc a c ⊆ uIcc a b ∪ uIcc b c

A sort of triangle inequality.

source
theorem Set.monotone_or_antitone_iff_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} :
Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ uIcc a b → f c ∈ uIcc (f a) (f b)
source
theorem Set.monotoneOn_or_antitoneOn_iff_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} :
MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ uIcc a b → f c ∈ uIcc (f a) (f b)
source
def Set.uIoc {α : Type u_1} [LinearOrder α] :
α → α → Set α

The open-closed uIcc with unordered bounds.

Equations

- Set.uIoc a b = Set.Ioc (min a b) (max a b)

Instances For

source
def Interval.termΙ :
Lean.ParserDescr

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

Equations

- Interval.termΙ = Lean.ParserDescr.node `Interval.termΙ 1024 (Lean.ParserDescr.symbol "Ι")

Instances For

source
@[simp]
theorem Set.uIoc_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
uIoc a b = Ioc a b
source
@[simp]
theorem Set.uIoc_of_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
uIoc a b = Ioc b a
source
theorem Set.uIoc_eq_union {α : Type u_1} [LinearOrder α] {a b : α} :
uIoc a b = Ioc a b ∪ Ioc b a
source
theorem Set.mem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} :
a ∈ uIoc b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
source
theorem Set.notMem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} :
a ∉ uIoc b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
source
@[deprecated Set.notMem_uIoc (since := "2025-05-23")]
theorem Set.not_mem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} :
a ∉ uIoc b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Alias of `Set.notMem_uIoc`.

source
@[simp]
theorem Set.left_mem_uIoc {α : Type u_1} [LinearOrder α] {a b : α} :
a ∈ uIoc a b ↔ b < a
source
@[simp]
theorem Set.right_mem_uIoc {α : Type u_1} [LinearOrder α] {a b : α} :
b ∈ uIoc a b ↔ a < b
source
theorem Set.forall_uIoc_iff {α : Type u_1} [LinearOrder α] {a b : α} {P : α → Prop} :
(∀ x ∈ uIoc a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x
source
theorem Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc {α : Type u_1} [LinearOrder α] {a b c d : α} (h : uIcc a b ⊆ uIcc c d) :
uIoc a b ⊆ uIoc c d
source
theorem Set.uIoc_comm {α : Type u_1} [LinearOrder α] (a b : α) :
uIoc a b = uIoc b a
source
theorem Set.Ioc_subset_uIoc {α : Type u_1} [LinearOrder α] {a b : α} :
Ioc a b ⊆ uIoc a b
source
theorem Set.Ioc_subset_uIoc' {α : Type u_1} [LinearOrder α] {a b : α} :
Ioc a b ⊆ uIoc b a
source
theorem Set.uIoc_subset_uIcc {α : Type u_1} [LinearOrder α] {a b : α} :
uIoc a b ⊆ uIcc a b
source
theorem Set.eq_of_mem_uIoc_of_mem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} :
a ∈ uIoc b c → b ∈ uIoc a c → a = b
source
theorem Set.eq_of_mem_uIoc_of_mem_uIoc' {α : Type u_1} [LinearOrder α] {a b c : α} :
b ∈ uIoc a c → c ∈ uIoc a b → b = c
source
theorem Set.eq_of_notMem_uIoc_of_notMem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a ≤ c) (hb : b ≤ c) :
a ∉ uIoc b c → b ∉ uIoc a c → a = b
source
@[deprecated Set.eq_of_notMem_uIoc_of_notMem_uIoc (since := "2025-05-23")]
theorem Set.eq_of_not_mem_uIoc_of_not_mem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a ≤ c) (hb : b ≤ c) :
a ∉ uIoc b c → b ∉ uIoc a c → a = b

Alias of `Set.eq_of_notMem_uIoc_of_notMem_uIoc`.

source
theorem Set.uIoc_injective_right {α : Type u_1} [LinearOrder α] (a : α) :
Function.Injective fun (b : α) => uIoc b a
source
theorem Set.uIoc_injective_left {α : Type u_1} [LinearOrder α] (a : α) :
Function.Injective (uIoc a)
source
theorem Set.uIoc_union_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} (h : b ∈ uIcc a c) :
uIoc a b ∪ uIoc b c = uIoc a c
source
def Set.uIoo {α : Type u_1} [LinearOrder α] (a b : α) :
Set α

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

Equations

- Set.uIoo a b = Set.Ioo (min a b) (max a b)

Instances For

source
@[simp]
theorem Set.uIoo_toDual {α : Type u_1} [LinearOrder α] (a b : α) :
uIoo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIoo a b
source
@[simp]
theorem Set.uIoo_ofDual {α : Type u_1} [LinearOrder α] (a b : α ᵒᵈ) :
uIoo (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' uIoo a b
source
@[simp]
theorem Set.uIoo_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) :
uIoo a b = Ioo a b
source
@[simp]
theorem Set.uIoo_of_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) :
uIoo a b = Ioo b a
source
theorem Set.uIoo_comm {α : Type u_1} [LinearOrder α] (a b : α) :
uIoo a b = uIoo b a
source
theorem Set.uIoo_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) :
uIoo a b = Ioo a b
source
theorem Set.uIoo_of_gt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) :
uIoo a b = Ioo b a
source
theorem Set.uIoo_self {α : Type u_1} [LinearOrder α] {a : α} :
uIoo a a = ∅
source
@[simp]
theorem Set.left_notMem_uIoo {α : Type u_1} [LinearOrder α] {a b : α} :
a ∉ uIoo a b
source
@[simp]
theorem Set.right_notMem_uIoo {α : Type u_1} [LinearOrder α] {a b : α} :
b ∉ uIoo a b
source
theorem Set.Ioo_subset_uIoo {α : Type u_1} [LinearOrder α] {a b : α} :
Ioo a b ⊆ uIoo a b
source
theorem Set.Ioo_subset_uIoo' {α : Type u_1} [LinearOrder α] {a b : α} :
Ioo b a ⊆ uIoo a b

Same as `Ioo_subset_uIoo` but with `Ioo a b` replaced by `Ioo b a`.

source
theorem Set.mem_uIoo_of_lt {α : Type u_1} [LinearOrder α] {a b x : α} (ha : a < x) (hb : x < b) :
x ∈ uIoo a b
source
theorem Set.mem_uIoo_of_gt {α : Type u_1} [LinearOrder α] {a b x : α} (hb : b < x) (ha : x < a) :
x ∈ uIoo a b
source
theorem Set.Ioo_min_max {α : Type u_1} [LinearOrder α] {a b : α} :
Ioo (min a b) (max a b) = uIoo a b
source
theorem Set.uIoo_of_not_le {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a ≤ b) :
uIoo a b = Ioo b a
source
theorem Set.uIoo_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) :
uIoo a b = Ioo a b
source
theorem Set.uIoo_subset_uIcc_self {α : Type u_1} [LinearOrder α] {a b : α} :
uIoo a b ⊆ uIcc a b
source
@[deprecated Set.uIoo_subset_uIcc_self (since := "2025-11-09")]
theorem Set.uIoo_subset_uIcc {α : Type u_1} [LinearOrder α] (a b : α) :
uIoo a b ⊆ uIcc a b
source
theorem Set.uIoo_subset_Ioo {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) :
uIoo a₁ b₁ ⊆ Ioo a₂ b₂
source
@[simp]
theorem Set.nonempty_uIoo {α : Type u_1} [LinearOrder α] {a b : α} [DenselyOrdered α] :
(uIoo a b).Nonempty ↔ a ≠ b
source
theorem Set.uIoo_eq_union {α : Type u_1} [LinearOrder α] {a b : α} :
uIoo a b = Ioo a b ∪ Ioo b a