mathlib3 documentation

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.uIcc_of_le {α : Type u_1} [lattice α] {a b : α} (h : a b) :
@[simp]
theorem set.uIcc_of_ge {α : Type u_1} [lattice α] {a b : α} (h : b a) :
theorem set.uIcc_comm {α : Type u_1} [lattice α] (a b : α) :
theorem set.uIcc_of_lt {α : Type u_1} [lattice α] {a b : α} (h : a < b) :
theorem set.uIcc_of_gt {α : Type u_1} [lattice α] {a b : α} (h : b < a) :
@[simp]
theorem set.uIcc_self {α : Type u_1} [lattice α] {a : α} :
set.uIcc 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 : α} :
theorem set.Icc_subset_uIcc' {α : Type u_1} [lattice α] {a b : α} :
@[simp]
theorem set.left_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :
@[simp]
theorem set.right_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :
theorem set.mem_uIcc_of_le {α : Type u_1} [lattice α] {a b x : α} (ha : a x) (hb : x b) :
theorem set.mem_uIcc_of_ge {α : Type u_1} [lattice α] {a b x : α} (hb : b x) (ha : x a) :
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 set.uIcc a b) :
theorem set.uIcc_subset_uIcc_left {α : Type u_1} [lattice α] {a b x : α} (h : x set.uIcc a b) :
theorem set.bdd_below_bdd_above_iff_subset_uIcc {α : Type u_1} [lattice α] (s : set α) :
bdd_below s bdd_above s (a b : α), s set.uIcc a 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 : α × β) :
theorem set.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [distrib_lattice α] {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} [distrib_lattice α] {a b c : α} :
b set.uIcc a c c set.uIcc a b b = c
theorem set.uIcc_injective_right {α : Type u_1} [distrib_lattice α] (a : α) :
function.injective (λ (b : α), set.uIcc b a)
theorem set.Icc_min_max {α : Type u_1} [linear_order α] {a b : α} :
theorem set.uIcc_of_not_le {α : Type u_1} [linear_order α] {a b : α} (h : ¬a b) :
theorem set.uIcc_of_not_ge {α : Type u_1} [linear_order α] {a b : α} (h : ¬b a) :
theorem set.uIcc_eq_union {α : Type u_1} [linear_order α] {a b : α} :
theorem set.mem_uIcc {α : Type u_1} [linear_order α] {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} [linear_order α] {a b c : α} (ha : c < a) (hb : c < b) :
theorem set.not_mem_uIcc_of_gt {α : Type u_1} [linear_order α] {a b c : α} (ha : a < c) (hb : b < c) :
theorem set.uIcc_subset_uIcc_iff_le {α : Type u_1} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
set.uIcc a₁ b₁ set.uIcc a₂ b₂ linear_order.min a₂ b₂ linear_order.min a₁ b₁ linear_order.max a₁ b₁ linear_order.max a₂ b₂
theorem set.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [linear_order α] {a 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 : α β} :
monotone f antitone f (a b c : α), c set.uIcc a 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 α} :
monotone_on f s antitone_on f s (a : α), a s (b : α), b s (c : α), c s c set.uIcc a 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) :
@[simp]
theorem set.uIoc_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : b < a) :
theorem set.uIoc_eq_union {α : Type u_1} [linear_order α] {a b : α} :
theorem set.mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a set.uIoc b c b < a a c c < a a b
theorem set.not_mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a set.uIoc b c a b a c c < a b < a
@[simp]
theorem set.left_mem_uIoc {α : Type u_1} [linear_order α] {a b : α} :
a set.uIoc a b b < a
@[simp]
theorem set.right_mem_uIoc {α : Type u_1} [linear_order α] {a b : α} :
b set.uIoc a b a < b
theorem set.forall_uIoc_iff {α : Type u_1} [linear_order α] {a b : α} {P : α Prop} :
( (x : α), x set.uIoc a b P x) ( (x : α), x set.Ioc a b P x) (x : α), x set.Ioc b a P x
theorem set.uIoc_subset_uIoc_of_uIcc_subset_uIcc {α : Type u_1} [linear_order α] {a b c d : α} (h : set.uIcc a b set.uIcc c d) :
theorem set.uIoc_swap {α : Type u_1} [linear_order α] (a b : α) :
theorem set.Ioc_subset_uIoc {α : Type u_1} [linear_order α] {a b : α} :
theorem set.Ioc_subset_uIoc' {α : Type u_1} [linear_order α] {a b : α} :
theorem set.eq_of_mem_uIoc_of_mem_uIoc {α : Type u_1} [linear_order α] {a b c : α} :
a set.uIoc b c b set.uIoc a c a = b
theorem set.eq_of_mem_uIoc_of_mem_uIoc' {α : Type u_1} [linear_order α] {a b c : α} :
b set.uIoc a c c set.uIoc a 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 set.uIoc b c b set.uIoc a c a = b
theorem set.uIoc_injective_right {α : Type u_1} [linear_order α] (a : α) :
function.injective (λ (b : α), set.uIoc b a)