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

set.uIcc a b = set.Icc (a ⊓ b) (a ⊔ b)

Instances for set.uIcc

Instances for ↥set.uIcc

set.fintype_uIcc

@[simp]

theorem set.dual_uIcc {α : Type u_1} [lattice α] (a b : α) :

set.uIcc (⇑order_dual.to_dual a) (⇑order_dual.to_dual b) = ⇑order_dual.of_dual ⁻¹' set.uIcc a b

@[simp]

theorem set.uIcc_of_le {α : Type u_1} [lattice α] {a b : α} (h : a ≤ b) :

set.uIcc a b = set.Icc a b

@[simp]

theorem set.uIcc_of_ge {α : Type u_1} [lattice α] {a b : α} (h : b ≤ a) :

set.uIcc a b = set.Icc b a

theorem set.uIcc_comm {α : Type u_1} [lattice α] (a b : α) :

set.uIcc a b = set.uIcc b a

theorem set.uIcc_of_lt {α : Type u_1} [lattice α] {a b : α} (h : a < b) :

set.uIcc a b = set.Icc a b

theorem set.uIcc_of_gt {α : Type u_1} [lattice α] {a b : α} (h : b < a) :

set.uIcc a b = set.Icc 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 : α} :

(set.uIcc a b).nonempty

theorem set.Icc_subset_uIcc {α : Type u_1} [lattice α] {a b : α} :

set.Icc a b ⊆ set.uIcc a b

theorem set.Icc_subset_uIcc' {α : Type u_1} [lattice α] {a b : α} :

set.Icc b a ⊆ set.uIcc a b

@[simp]

theorem set.left_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :

a ∈ set.uIcc a b

@[simp]

theorem set.right_mem_uIcc {α : Type u_1} [lattice α] {a b : α} :

b ∈ set.uIcc a b

theorem set.mem_uIcc_of_le {α : Type u_1} [lattice α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) :

x ∈ set.uIcc a b

theorem set.mem_uIcc_of_ge {α : Type u_1} [lattice α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) :

x ∈ set.uIcc a 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 ∈ set.uIcc a b) :

set.uIcc x b ⊆ set.uIcc a b

theorem set.uIcc_subset_uIcc_left {α : Type u_1} [lattice α] {a b x : α} (h : x ∈ set.uIcc a b) :

set.uIcc a 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 : α × β) :

set.uIcc a b = set.uIcc a.fst b.fst ×ˢ set.uIcc a.snd b.snd

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.uIcc_injective_left {α : Type u_1} [distrib_lattice α] (a : α) :

function.injective (set.uIcc a)

theorem monotone_on.image_uIcc_subset {α : Type u_1} {β : Type u_2} [linear_order α] [lattice β] {f : α → β} {a b : α} (hf : monotone_on f (set.uIcc a b)) :

f '' set.uIcc a 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 : antitone_on 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} [linear_order α] [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} [linear_order α] [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} [linear_order α] {a b : α} :

set.Icc (linear_order.min a b) (linear_order.max a b) = set.uIcc a b

theorem set.uIcc_of_not_le {α : Type u_1} [linear_order α] {a b : α} (h : ¬a ≤ b) :

set.uIcc a b = set.Icc b a

theorem set.uIcc_of_not_ge {α : Type u_1} [linear_order α] {a b : α} (h : ¬b ≤ a) :

set.uIcc a b = set.Icc a b

theorem set.uIcc_eq_union {α : Type u_1} [linear_order α] {a b : α} :

set.uIcc a b = set.Icc a b ∪ set.Icc b a

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

c ∉ set.uIcc a b

theorem set.not_mem_uIcc_of_gt {α : Type u_1} [linear_order α] {a b c : α} (ha : a < c) (hb : b < c) :

c ∉ set.uIcc a 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₂ ↔ 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 : α} :

set.uIcc a c ⊆ set.uIcc a b ∪ set.uIcc 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

set.uIoc = λ (a b : α), set.Ioc (linear_order.min a b) (linear_order.max a b)

Instances for set.uIoc

set.ord_connected_uIoc

@[simp]

theorem set.uIoc_of_le {α : Type u_1} [linear_order α] {a b : α} (h : a ≤ b) :

set.uIoc a b = set.Ioc a b

@[simp]

theorem set.uIoc_of_lt {α : Type u_1} [linear_order α] {a b : α} (h : b < a) :

set.uIoc a b = set.Ioc b a

theorem set.uIoc_eq_union {α : Type u_1} [linear_order α] {a b : α} :

set.uIoc a b = set.Ioc a b ∪ set.Ioc b a

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

set.uIoc a b ⊆ set.uIoc c d

theorem set.uIoc_swap {α : Type u_1} [linear_order α] (a b : α) :

set.uIoc a b = set.uIoc b a

theorem set.Ioc_subset_uIoc {α : Type u_1} [linear_order α] {a b : α} :

set.Ioc a b ⊆ set.uIoc a b

theorem set.Ioc_subset_uIoc' {α : Type u_1} [linear_order α] {a b : α} :

set.Ioc a b ⊆ set.uIoc b a

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)

theorem set.uIoc_injective_left {α : Type u_1} [linear_order α] (a : α) :

function.injective (set.uIoc a)