Set.right_mem_uIcc
theorem Set.right_mem_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, b ∈ Set.uIcc a b
This theorem states that for any lattice `α` and any elements `a` and `b` of `α`, the element `b` is included in the set `Set.uIcc a b`. In other words, in any lattice, the upper boundary of the set defined by the least upper bound (join/supremum) and greatest lower bound (meet/infimum) of `a` and `b` always includes `b`.
More concisely: For any lattice and elements `a` and `b`, the greatest lower bound of `a` and `b` is a lower bound of `b`, and the least upper bound of `a` and `b` is an upper bound of `b`. Therefore, `b` belongs to the interval `[a, b]` defined by `Set.uIcc a b`.
|
Set.not_mem_uIcc_of_lt
theorem Set.not_mem_uIcc_of_lt :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c < a → c < b → c ∉ Set.uIcc a b
The theorem `Set.not_mem_uIcc_of_lt` states that for any type `α` that has a linear order and for any three elements `a`, `b`, and `c` of this type, if `c` is less than `a` and `c` is also less than `b`, then `c` does not belong to the set `uIcc a b`. The set `uIcc a b` is defined as the set of all elements that lie between `a` and `b`, inclusive of `a` and `b` themselves. In other words, `c` cannot be in the set `uIcc a b` if `c` is less than both `a` and `b`.
More concisely: For any type `α` with a linear order and any elements `a`, `b`, and `c` of `α`, if `c` is strictly less than both `a` and `b`, then `c` is not in the interval `[a, b]` (denoted `uIcc a b` in Lean) consisting of elements between `a` and `b` inclusive.
|
Set.uIoc_eq_union
theorem Set.uIoc_eq_union : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Ι a b = Set.Ioc a b ∪ Set.Ioc b a := by
sorry
The theorem `Set.uIoc_eq_union` states that for any type `α` with a linear order, and any two elements `a` and `b` of `α`, the unordered interval `Ι a b` is equal to the union of the left-open right-closed interval from `a` to `b`, denoted `Set.Ioc a b`, and the left-open right-closed interval from `b` to `a`, denoted `Set.Ioc b a`. In mathematical terms, this means that any element in the unordered interval between `a` and `b` is either greater than `a` and less than or equal to `b`, or greater than `b` and less than or equal to `a`.
More concisely: For any type with a linear order, the unordered interval between two elements is equal to the union of the left-open right-closed intervals from each element to the other.
|
Set.uIcc_of_le
theorem Set.uIcc_of_le : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a ≤ b → Set.uIcc a b = Set.Icc a b
The theorem `Set.uIcc_of_le` states that for any type `α` that has a `Lattice` structure, and for any two elements `a` and `b` of this type, if `a` is less than or equal to `b`, then the universal bounded lattice of `a` and `b`, denoted by `Set.uIcc a b`, is equal to the closed interval between `a` and `b`, denoted by `Set.Icc a b`. Here, `Set.uIcc a b` represents the set of all elements lying between `a` and `b` with both `a` and `b` included, and `Set.Icc a b` represents the left-closed right-closed interval from `a` to `b`.
More concisely: For any type `α` with a `Lattice` structure and elements `a` and `b`, if `a ≤ b`, then `Set.uIcc a b = Set.Icc a b`.
|
Set.uIcc_of_ge
theorem Set.uIcc_of_ge : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, b ≤ a → Set.uIcc a b = Set.Icc b a
The theorem `Set.uIcc_of_ge` states that for any type `α` that forms a lattice, and for any two elements `a` and `b` of this type, if `b` is less than or equal to `a`, then the set of elements lying between `a` and `b` with both `a` and `b` included (`Set.uIcc a b`), is equal to the set of elements lying between `b` and `a` with both `b` and `a` included (`Set.Icc b a`). Essentially, it asserts that the interval from `a` to `b` is the same as the interval from `b` to `a` when `b` is less than or equal to `a` in a lattice structure.
More concisely: For any lattice type `α` and elements `a` and `b` with `b ≤ a`, `Set.uIcc a b` equals `Set.Icc b a`.
|
Set.uIcc_comm
theorem Set.uIcc_comm : ∀ {α : Type u_1} [inst : Lattice α] (a b : α), Set.uIcc a b = Set.uIcc b a
The theorem `Set.uIcc_comm` states that for any type `α` that forms a lattice, and for any two elements `a` and `b` of this type, the set of elements lying between `a` and `b`, with `a` and `b` included (`Set.uIcc a b`), is equivalent to the set of elements lying between `b` and `a`, with `b` and `a` included (`Set.uIcc b a`). This asserts the commutativity of the bounded interval function `uIcc` in the context of a lattice, meaning it doesn't matter which order the elements are given in, the resulting set is the same.
More concisely: For any lattice type `α` and elements `a` and `b` in `α`, the upward closed intervals `Set.uIcc a b` and `Set.uIcc b a` are equal.
|
Set.uIoc_of_lt
theorem Set.uIoc_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b < a → Ι a b = Set.Ioc b a
This theorem states that for any type `α` that has a linear order and for any two elements `a` and `b` of this type, if `b` is less than `a` then `Ι a b` equals the left-open right-closed interval from `b` to `a`. In other words, the set `Ι a b` includes all elements `x` such that `b` is less than `x` and `x` is less than or equal to `a`.
More concisely: For any type `α` with a linear order and any `a` and `b` in `α` with `b < a`, the interval `Ι a b` is the set of elements `x` such that `b < x <= a`.
|
Set.not_mem_uIcc_of_gt
theorem Set.not_mem_uIcc_of_gt :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < c → b < c → c ∉ Set.uIcc a b
This theorem states that for any type `α` with a linear order, and for any three elements `a`, `b`, and `c` of type `α`, if `c` is greater than both `a` and `b`, then `c` is not in the set `uIcc a b`. Here `uIcc a b` represents the set of elements lying between `a` and `b`, inclusive. In other words, if `c` is strictly greater than both ends of a closed interval, it does not belong to that interval.
More concisely: For any linear order type `α` and elements `a`, `b`, `c` in `α`, if `c` is strictly greater than both `a` and `b`, then `c` is not in the closed interval `[a, b]`.
|
Set.uIcc_subset_uIcc_union_uIcc
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
The theorem titled "A sort of triangle inequality" states the following: For any type 'α' that has a linear order, and for any three elements 'a', 'b', and 'c' of type 'α', the set of elements that lie between 'a' and 'c' inclusive is a subset of the union of the set of elements that lie between 'a' and 'b' inclusive and the set of elements that lie between 'b' and 'c' inclusive. In other words, it is stating a property similar to the triangle inequality but for sets, where the set from 'a' to 'c' is contained in the combined set from 'a' to 'b' and 'b' to 'c'.
More concisely: For any type 'α' with a linear order, the set of elements between 'a' and 'c' (inclusive) is contained in the union of the sets between 'a' and 'b' (inclusive) and between 'b' and 'c' (inclusive).
|
Set.Icc_subset_uIcc
theorem Set.Icc_subset_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, Set.Icc a b ⊆ Set.uIcc a b
This theorem states that for any type `α` equipped with a lattice structure, and for any two elements `a` and `b` in `α`, the interval `Set.Icc a b` is a subset of the interval `Set.uIcc a b`. Here, `Set.Icc a b` represents the set of elements lying between `a` and `b`, inclusive, in the given order, whereas `Set.uIcc a b` represents a set of elements lying between the minimum (`a ⊓ b`) and the maximum (`a ⊔ b`) of `a` and `b`, inclusive. This theorem essentially asserts that any element that lies between `a` and `b` in the specified order will also lie between the minimum and maximum of `a` and `b`, inclusive.
More concisely: For any lattice `α` and elements `a` and `b` in `α`, `Set.Icc a b` is included in `Set.uIcc a b`. That is, all elements between `a` and `b` in order are also between their minimum and maximum in the lattice.
|
Set.left_mem_uIcc
theorem Set.left_mem_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a ∈ Set.uIcc a b
The theorem `Set.left_mem_uIcc` states that for any type `α` that forms a lattice, given any two elements `a` and `b` of `α`, `a` is always an element of the set `Set.uIcc a b`. Here, `Set.uIcc a b` represents the set of all elements lying between `a` and `b` (inclusive), where the notion of betweenness is based on the lattice structure of `α`.
More concisely: For any lattice type `α` and elements `a` and `b` in `α`, `a` is in the interval `Set.uIcc a b`.
|
Set.uIoc_of_le
theorem Set.uIoc_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Ι a b = Set.Ioc a b
This theorem states that for any type `α` with a linear order, and any two elements `a` and `b` of that type, if `a` is less than or equal to `b`, then the half-open interval from `a` to `b`, denoted `Ι a b`, is equal to the left-open right-closed interval from `a` to `b`, denoted `Set.Ioc a b`. In other words, if `a` and `b` are elements of a type with a linear order and `a ≤ b`, then the set of all elements `x` such that `a < x` and `x ≤ b` is the same whether you consider it as a half-open interval or as a left-open right-closed interval.
More concisely: For any type with a linear order, the half-open interval [a, b] equals the left-open right-closed interval (a, b] if a ≤ b.
|
Set.uIcc_subset_uIcc
theorem Set.uIcc_subset_uIcc :
∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
a₁ ∈ Set.uIcc a₂ b₂ → b₁ ∈ Set.uIcc a₂ b₂ → Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂
The theorem `Set.uIcc_subset_uIcc` states that for any lattice type `α`, and any four elements `a₁`, `a₂`, `b₁`, and `b₂` of this type, if `a₁` is within the set of elements lying between `a₂` and `b₂` (inclusive) and `b₁` is also within this set, then the set of elements between `a₁` and `b₁` (inclusive) is a subset of the set of elements between `a₂` and `b₂` (inclusive). In other words, if `a₁` and `b₁` are both in the bounding box defined by `a₂` and `b₂`, then the bounding box defined by `a₁` and `b₁` is contained within the bounding box defined by `a₂` and `b₂`.
More concisely: For any lattice type `α` and elements `a₁`, `a₂`, `b₁`, and `b₂` in `α`, if `a₁` and `b₁` are within the interval `[a₂, b₂]`, then `[a₁, b₁]` is a subset of `[a₂, b₂]`.
|
Set.uIoc_comm
theorem Set.uIoc_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), Ι a b = Ι b a
This theorem, `Set.uIoc_comm`, states that for any type `α` that has a linear order, the interval `Ι a b` (which represents the set of all elements between `a` and `b`) is the same as the interval `Ι b a`. In other words, the order of `a` and `b` does not matter when defining an interval between them.
More concisely: For any type `α` with a linear order, the interval `Ι a b` equals `Ι b a`.
|
Set.eq_of_mem_uIcc_of_mem_uIcc
theorem Set.eq_of_mem_uIcc_of_mem_uIcc :
∀ {α : Type u_1} [inst : DistribLattice α] {a b c : α}, a ∈ Set.uIcc b c → b ∈ Set.uIcc a c → a = b
This theorem states that for any type `α` that forms a distributive lattice, given three elements `a`, `b`, and `c` of `α`, if `a` lies in the set of elements between `b` and `c` (inclusive), and `b` lies in the set of elements between `a` and `c` (inclusive), then `a` and `b` must be equal. This is a property of the `Set.uIcc` function, which defines the set of elements between two given elements in a lattice.
More concisely: In a distributive lattice, if `a` is between `b` and `c`, and `b` is between `a` and `c`, then `a = b`.
|