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} [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.

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

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

@[simp]

theorem Set.uIcc_toDual {α : Type u_1} [Lattice α] (a b : α) : uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIcc a b

@[deprecated Set.uIcc_toDual (since := "2025-03-20")]

theorem Set.dual_uIcc {α : Type u_1} [Lattice α] (a b : α) : uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIcc a b

Alias of Set.uIcc_toDual.

@[simp]

theorem Set.uIcc_ofDual {α : Type u_1} [Lattice α] (a b : αᵒᵈ) : uIcc (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' uIcc a b

@[simp]

theorem Set.uIcc_of_le {α : Type u_1} [Lattice α] {a b : α} (h : a ≤ b) : uIcc a b = Icc a b

@[simp]

theorem Set.uIcc_of_ge {α : Type u_1} [Lattice α] {a b : α} (h : b ≤ a) : uIcc a b = Icc b a

theorem Set.uIcc_comm {α : Type u_1} [Lattice α] (a b : α) : uIcc a b = uIcc b a

theorem Set.uIcc_of_lt {α : Type u_1} [Lattice α] {a b : α} (h : a < b) : uIcc a b = Icc a b

theorem Set.uIcc_of_gt {α : Type u_1} [Lattice α] {a b : α} (h : b < a) : uIcc a b = Icc b a

theorem Set.uIcc_self {α : Type u_1} [Lattice α] {a : α} : uIcc a a = {a}

@[simp]

theorem Set.nonempty_uIcc {α : Type u_1} [Lattice α] {a b : α} : (uIcc a b).Nonempty

theorem Set.Icc_subset_uIcc {α : Type u_1} [Lattice α] {a b : α} : Icc a b ⊆ uIcc a b

theorem Set.Icc_subset_uIcc' {α : Type u_1} [Lattice α] {a b : α} : Icc b a ⊆ uIcc a b

@[simp]

theorem Set.left_mem_uIcc {α : Type u_1} [Lattice α] {a b : α} : a ∈ uIcc a b

@[simp]

theorem Set.right_mem_uIcc {α : Type u_1} [Lattice α] {a b : α} : b ∈ uIcc a b

theorem Set.mem_uIcc_of_le {α : Type u_1} [Lattice α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) : x ∈ uIcc a b

theorem Set.mem_uIcc_of_ge {α : Type u_1} [Lattice α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) : x ∈ uIcc a b

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₂

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₂

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₂

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₂

theorem Set.uIcc_subset_uIcc_right {α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ uIcc a b) : uIcc x b ⊆ uIcc a b

theorem Set.uIcc_subset_uIcc_left {α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ uIcc a b) : uIcc a x ⊆ uIcc a b

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

@[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₂)

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

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

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

theorem Set.uIcc_injective_right {α : Type u_1} [DistribLattice α] (a : α) : Function.Injective fun (b : α) => uIcc b a

theorem Set.uIcc_injective_left {α : Type u_1} [DistribLattice α] (a : α) : Function.Injective (uIcc a)

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))

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))

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))

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))

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)

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)

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)

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)

theorem Set.Icc_min_max {α : Type u_1} [LinearOrder α] {a b : α} : Icc (min a b) (max a b) = uIcc a b

theorem Set.uIcc_of_not_le {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a ≤ b) : uIcc a b = Icc b a

theorem Set.uIcc_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) : uIcc a b = Icc a b

theorem Set.uIcc_eq_union {α : Type u_1} [LinearOrder α] {a b : α} : uIcc a b = Icc a b ∪ Icc b a

theorem Set.mem_uIcc {α : Type u_1} [LinearOrder α] {a b c : α} : a ∈ uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

theorem Set.notMem_uIcc_of_lt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : c < a) (hb : c < b) : c ∉ uIcc a b

@[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.

theorem Set.notMem_uIcc_of_gt {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a < c) (hb : b < c) : c ∉ uIcc a b

@[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.

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₂

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.

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)

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)

def Set.uIoc {α : Type u_1} [LinearOrder α] : α → α → Set α

The open-closed uIcc with unordered bounds.

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.

@[simp]

theorem Set.uIoc_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : uIoc a b = Ioc a b

@[simp]

theorem Set.uIoc_of_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) : uIoc a b = Ioc b a

theorem Set.uIoc_eq_union {α : Type u_1} [LinearOrder α] {a b : α} : uIoc a b = Ioc a b ∪ Ioc b a

theorem Set.mem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} : a ∈ uIoc b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

theorem Set.notMem_uIoc {α : Type u_1} [LinearOrder α] {a b c : α} : a ∉ uIoc b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

@[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.

@[simp]

theorem Set.left_mem_uIoc {α : Type u_1} [LinearOrder α] {a b : α} : a ∈ uIoc a b ↔ b < a

@[simp]

theorem Set.right_mem_uIoc {α : Type u_1} [LinearOrder α] {a b : α} : b ∈ uIoc a b ↔ a < b

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

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

theorem Set.uIoc_comm {α : Type u_1} [LinearOrder α] (a b : α) : uIoc a b = uIoc b a

theorem Set.Ioc_subset_uIoc {α : Type u_1} [LinearOrder α] {a b : α} : Ioc a b ⊆ uIoc a b

theorem Set.Ioc_subset_uIoc' {α : Type u_1} [LinearOrder α] {a b : α} : Ioc a b ⊆ uIoc b a

theorem Set.uIoc_subset_uIcc {α : Type u_1} [LinearOrder α] {a b : α} : uIoc a b ⊆ uIcc a b

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

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

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

@[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.

theorem Set.uIoc_injective_right {α : Type u_1} [LinearOrder α] (a : α) : Function.Injective fun (b : α) => uIoc b a

theorem Set.uIoc_injective_left {α : Type u_1} [LinearOrder α] (a : α) : Function.Injective (uIoc a)

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

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.

@[simp]

theorem Set.uIoo_toDual {α : Type u_1} [LinearOrder α] (a b : α) : uIoo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIoo a b

@[deprecated Set.uIoo_toDual (since := "2025-03-20")]

theorem Set.dual_uIoo {α : Type u_1} [LinearOrder α] (a b : α) : uIoo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' uIoo a b

Alias of Set.uIoo_toDual.

@[simp]

theorem Set.uIoo_ofDual {α : Type u_1} [LinearOrder α] (a b : αᵒᵈ) : uIoo (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' uIoo a b

@[simp]

theorem Set.uIoo_of_le {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : uIoo a b = Ioo a b

@[simp]

theorem Set.uIoo_of_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) : uIoo a b = Ioo b a

theorem Set.uIoo_comm {α : Type u_1} [LinearOrder α] (a b : α) : uIoo a b = uIoo b a

theorem Set.uIoo_of_lt {α : Type u_1} [LinearOrder α] {a b : α} (h : a < b) : uIoo a b = Ioo a b

theorem Set.uIoo_of_gt {α : Type u_1} [LinearOrder α] {a b : α} (h : b < a) : uIoo a b = Ioo b a

theorem Set.uIoo_self {α : Type u_1} [LinearOrder α] {a : α} : uIoo a a = ∅

theorem Set.Ioo_subset_uIoo {α : Type u_1} [LinearOrder α] {a b : α} : Ioo a b ⊆ uIoo a b

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.

theorem Set.mem_uIoo_of_lt {α : Type u_1} [LinearOrder α] {a b x : α} (ha : a < x) (hb : x < b) : x ∈ uIoo a b

theorem Set.mem_uIoo_of_gt {α : Type u_1} [LinearOrder α] {a b x : α} (hb : b < x) (ha : x < a) : x ∈ uIoo a b

theorem Set.Ioo_min_max {α : Type u_1} [LinearOrder α] {a b : α} : Ioo (min a b) (max a b) = uIoo a b

theorem Set.uIoo_of_not_le {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a ≤ b) : uIoo a b = Ioo b a

theorem Set.uIoo_of_not_ge {α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) : uIoo a b = Ioo a b

theorem Set.uIoo_subset_uIcc {α : Type u_3} [LinearOrder α] (a b : α) : uIoo a b ⊆ uIcc a b