Documentation

Mathlib.Data.Set.Intervals.UnorderedInterval

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} [inst : 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)

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.

@[simp]

theorem Set.dual_uIcc {α : Type u_1} [inst : Lattice α] (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} [inst : Lattice α] {a : α} {b : α} (h : a ≤ b) :

Set.uIcc a b = Set.Icc a b

@[simp]

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

Set.uIcc a b = Set.Icc b a

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

Set.uIcc a b = Set.uIcc b a

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

Set.uIcc a b = Set.Icc a b

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

Set.uIcc a b = Set.Icc b a

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

Set.uIcc a a = {a}

@[simp]

theorem Set.nonempty_uIcc {α : Type u_1} [inst : Lattice α] {a : α} {b : α} :

Set.Nonempty (Set.uIcc a b)

theorem Set.Icc_subset_uIcc {α : Type u_1} [inst : Lattice α] {a : α} {b : α} :

Set.Icc a b ⊆ Set.uIcc a b

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

Set.Icc b a ⊆ Set.uIcc a b

@[simp]

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

a ∈ Set.uIcc a b

@[simp]

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

b ∈ Set.uIcc a b

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

x ∈ Set.uIcc a b

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

x ∈ Set.uIcc a b

theorem Set.uIcc_subset_uIcc {α : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Lattice α] (s : Set α) :

BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.uIcc a b

theorem Set.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [inst : DistribLattice α] {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} [inst : DistribLattice α] {a : α} {b : α} {c : α} :

b ∈ Set.uIcc a c → c ∈ Set.uIcc a b → b = c

theorem Set.uIcc_injective_right {α : Type u_1} [inst : DistribLattice α] (a : α) :

Function.Injective fun b => Set.uIcc b a

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

Function.Injective (Set.uIcc a)

theorem Set.Icc_min_max {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

Set.Icc (min a b) (max a b) = Set.uIcc a b

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

Set.uIcc a b = Set.Icc b a

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

Set.uIcc a b = Set.Icc a b

theorem Set.uIcc_eq_union {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a

theorem Set.mem_uIcc {α : Type u_1} [inst : LinearOrder α] {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} [inst : LinearOrder α] {a : α} {b : α} {c : α} (ha : c < a) (hb : c < b) :

¬c ∈ Set.uIcc a b

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

¬c ∈ Set.uIcc a b

theorem Set.uIcc_subset_uIcc_iff_le {α : Type u_1} [inst : LinearOrder α] {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} [inst : LinearOrder α] {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} [inst : LinearOrder α] [inst : LinearOrder β] {f : α → β} :

Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)

theorem Set.monotoneOn_or_antitoneOn_iff_uIcc {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : LinearOrder β] {f : α → β} {s : Set α} :

MonotoneOn f s ∨ AntitoneOn 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} [inst : LinearOrder α] :

α → α → Set α

The open-closed uIcc with unordered bounds.

Equations

Ι a b = Set.Ioc (min a b) (max a b)

def Set.termΙ :

Lean.ParserDescr

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

Equations

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

@[simp]

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

Ι a b = Set.Ioc a b

@[simp]

theorem Set.uIoc_of_lt {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} (h : b < a) :

Ι a b = Set.Ioc b a

theorem Set.uIoc_eq_union {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

Ι a b = Set.Ioc a b ∪ Set.Ioc b a

theorem Set.mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {c : α} :

a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

theorem Set.not_mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {c : α} :

¬a ∈ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

@[simp]

theorem Set.left_mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

a ∈ Ι a b ↔ b < a

@[simp]

theorem Set.right_mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

b ∈ Ι a b ↔ a < b

theorem Set.forall_uIoc_iff {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {P : α → Prop} :

((x : α) → x ∈ Ι 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} [inst : LinearOrder α] {a : α} {b : α} {c : α} {d : α} (h : Set.uIcc a b ⊆ Set.uIcc c d) :

Ι a b ⊆ Ι c d

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

Ι a b = Ι b a

theorem Set.Ioc_subset_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} :

Set.Ioc a b ⊆ Ι a b

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

Set.Ioc a b ⊆ Ι b a

theorem Set.eq_of_mem_uIoc_of_mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {c : α} :

a ∈ Ι b c → b ∈ Ι a c → a = b

theorem Set.eq_of_mem_uIoc_of_mem_uIoc' {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {c : α} :

b ∈ Ι a c → c ∈ Ι a b → b = c

theorem Set.eq_of_not_mem_uIoc_of_not_mem_uIoc {α : Type u_1} [inst : LinearOrder α] {a : α} {b : α} {c : α} (ha : a ≤ c) (hb : b ≤ c) :

¬a ∈ Ι b c → ¬b ∈ Ι a c → a = b

theorem Set.uIoc_injective_right {α : Type u_1} [inst : LinearOrder α] (a : α) :

Function.Injective fun b => Ι b a

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

Function.Injective (Ι a)