Set.Ico_subset_Ioo_left
theorem Set.Ico_subset_Ioo_left :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ < a₂ → Set.Ico a₂ b ⊆ Set.Ioo a₁ b
The theorem `Set.Ico_subset_Ioo_left` states that for any type `α` that has a pre-order relation defined, given three elements `a₁`, `a₂`, and `b` of type `α` where `a₁` is less than `a₂`, the left-closed right-open interval `[a₂, b)` is a subset of the left-open right-open interval `(a₁, b)`. This means all elements `x` that satisfy the inequality `a₂ ≤ x < b` also satisfy `a₁ < x < b`.
More concisely: For any pre-ordered type `α` and elements `a₁ < a₂` of `α`, the interval `[a₂, b)` is a subset of `(a₁, b)`. That is, for all `x`, if `a₂ ≤ x < b`, then `a₁ < x < b`.
|
Set.Ici_bot
theorem Set.Ici_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], Set.Ici ⊥ = Set.univ
The theorem `Set.Ici_bot` states that for any type `α` that has a preorder and a least element (denoted `⊥`), the left-closed right-infinite interval starting from that least element (`Set.Ici ⊥`) is equal to the universal set (`Set.univ`). In other words, for such an ordered type, the interval of all elements greater than or equal to the least element includes every element in the type, which is the definition of the universal set.
More concisely: For any type with a preorder and a least element, the set of elements greater than or equal to the least element is equal to the universal set.
|
Set.dual_Ioo
theorem Set.dual_Ioo :
∀ {α : Type u_1} [inst : Preorder α] {a b : α},
Set.Ioo (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioo b a
The theorem `Set.dual_Ioo` states that for any type `α` with a preorder relation, and any two elements `a` and `b` of this type, the left-open right-open interval in the dual order between `a` and `b` (that is, the set of elements `x` such that `a < x < b` under the dual order) is the preimage under the function `OrderDual.ofDual` of the left-open right-open interval between `b` and `a` in the original order. In other words, if we reverse the order of `a` and `b` and then apply `ofDual` to each element, we get the original interval between `a` and `b`.
More concisely: The dual order interval `(a, b)` in a preordered type equals the preimage of the original order interval `(b, a)` under the `OrderDual.ofDual` function.
|
Set.Iic_diff_right
theorem Set.Iic_diff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iic a \ {a} = Set.Iio a
This theorem states that for any partially ordered set, the difference between the left-infinite right-closed interval up to a point "a" and the singleton set containing "a" is equal to the left-infinite right-open interval up to "a". In other words, if you remove the end point "a" from the interval including "a" (denoted as Set.Iic a), you get the interval that does not include "a" (denoted as Set.Iio a). The intervals are defined over any type `α` that has a partial order (not necessarily a total order).
More concisely: For any partially ordered set, the difference between the left-infinite right-closed interval and the singleton set of a point is equal to the left-infinite right-open interval for that point.
|
Set.Icc_union_Icc
theorem Set.Icc_union_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
min a b < max c d → min c d < max a b → Set.Icc a b ∪ Set.Icc c d = Set.Icc (min a c) (max b d)
This theorem states that for any linearly ordered type `α` and any four elements `a`, `b`, `c`, and `d` of `α`, if the minimum of `a` and `b` is less than the maximum of `c` and `d`, and the minimum of `c` and `d` is less than the maximum of `a` and `b`, then the union of the closed interval from `a` to `b` and the closed interval from `c` to `d` is equal to the closed interval from the minimum of `a` and `c` to the maximum of `b` and `d`.
The theorem also adds a note that we cannot replace the `<` operator with `≤` in the hypotheses. If we did so, for `b < a = d < c` the left hand side would be an empty set and the right hand side would be the set containing `a`.
More concisely: For any linearly ordered type `α` and elements `a, b, c, d ∈ α` with `a < b < min(c, d) < max(a, b) < c < d`, the interval `[a, b] ∪ [c, d]` equals the interval `[min(a, c), max(b, d)]`.
Note: This theorem assumes the given hypotheses, and the inequality relations cannot be weakened to `≤`.
|
Set.Iic_inter_Iic
theorem Set.Iic_inter_Iic :
∀ {α : Type u_1} [inst : SemilatticeInf α] {a b : α}, Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)
The theorem `Set.Iic_inter_Iic` states that for any type `α` with an instance of `SemilatticeInf` (which means `α` has a binary operation "meet" or "infimum"), and for any elements `a` and `b` of type `α`, the intersection of the set of elements less than or equal to `a` (`Set.Iic a`) and the set of elements less than or equal to `b` (`Set.Iic b`) is equal to the set of elements less than or equal to the infimum of `a` and `b` (`Set.Iic (a ⊓ b)`). In other words, the common set of elements that are less than or equal to both `a` and `b` is exactly the set of elements that are less than or equal to their infimum.
More concisely: For any semilattice type `α` and elements `a` and `b` of `α`, `Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)`.
|
Set.Ioo_subset_Ico_self
theorem Set.Ioo_subset_Ico_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Ico a b
The theorem `Set.Ioo_subset_Ico_self` states that for any type `α` with a preorder structure and any two elements `a` and `b` of that type, the left-open right-open interval `(a, b)`, denoted as `Set.Ioo a b`, is a subset of the left-closed right-open interval `[a, b)`, denoted as `Set.Ico a b`. In other words, all elements `x` satisfying `a < x < b` also satisfy `a ≤ x < b`.
More concisely: For any type `α` with a preorder structure and any `a < b` in `α`, the left-open right-open interval `(a, b)` is included in the left-closed right-open interval `[a, b)`.
|
Set.Ioi_subset_Ici_self
theorem Set.Ioi_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi a ⊆ Set.Ici a
The theorem `Set.Ioi_subset_Ici_self` states that for any type `α` which is a preorder, and any element `a` of type `α`, the set of all elements which are strictly greater than `a` (`Set.Ioi a`) is a subset of the set of all elements which are greater than or equal to `a` (`Set.Ici a`). In other words, if an element is in the left-open right-infinite interval `(a, +∞)`, it is also in the left-closed right-infinite interval `[a, +∞)`.
More concisely: For any preorder type `α` and its element `a`, `Set.Ioi a` (strictly greater elements) is a subset of `Set.Ici a` (greater than or equal elements).
|
Set.Ioo_eq_empty
theorem Set.Ioo_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a < b → Set.Ioo a b = ∅
This theorem states that for any type `α` equipped with a preorder, the left-open right-open interval `(a, b)` (represented as `Set.Ioo a b`) is empty if `a` is not less than `b`. In other words, if `a` is greater than or equal to `b`, then there are no elements `x` such that `a < x < b`. This is a very intuitive result, since it simply says that in a given ordered set, there cannot be elements between two points if the first point is not strictly less than the second one.
More concisely: For any type `α` with a preorder, the left-open right-open interval `(a, b)` is empty when `a ≥ b`.
|
Set.Icc_eq_empty_iff
theorem Set.Icc_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b = ∅ ↔ ¬a ≤ b
The theorem `Set.Icc_eq_empty_iff` states that for any type `α` that has a preorder, and any two elements `a` and `b` of this type, the interval from `a` to `b` (i.e., the set of all `x` such that `a ≤ x ≤ b`) is empty if and only if `a` is not less than or equal to `b`. In mathematical terms, this says that an interval `[a, b]` is empty if and only if `a > b`.
More concisely: For any type with a preorder, the interval between two elements is empty if and only if one element is strictly greater than the other.
|
Set.left_mem_Ici
theorem Set.left_mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∈ Set.Ici a
The theorem `Set.left_mem_Ici` states that for all types `α` that have a `Preorder` structure, any element `a` of type `α` belongs to the set that represents the interval from `a` to infinity, inclusive. In other words, it asserts that `a` is always included in the interval `[a, ∞)` in any preordered set.
More concisely: For any preordered type `α` and element `a` in `α`, `a` belongs to the interval `[a, ∞)`.
|
Set.Ioc_eq_empty
theorem Set.Ioc_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a < b → Set.Ioc a b = ∅
The theorem `Set.Ioc_eq_empty` states that for any type `α` that has a predefined order, and for any two elements `a` and `b` in `α`, if `a` is not less than `b`, then the left-open right-closed interval from `a` to `b` is an empty set. In mathematical terms, if `a` is not less than `b` (i.e., `a ≥ b`), then the set of elements `x` such that `a < x ≤ b` is empty.
More concisely: If `α` is a type with a predefined order and `a ≥ b` in `α`, then the set `{x : α | a < x ≤ b}` is empty.
|
Set.left_mem_Icc
theorem Set.left_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Icc a b ↔ a ≤ b
This theorem states that for any type `α` with an associated `Preorder` instance, and any two elements `a` and `b` of the type `α`, `a` is an element of the left-closed right-closed interval from `a` to `b` (`Set.Icc a b`) if and only if `a` is less than or equal to `b`. In mathematical terms, it says that $a$ is in the closed interval $[a, b]$ if and only if $a \leq b$.
More concisely: For any type `α` with a `Preorder` instance, and any `α` elements `a` and `b`, `a` belongs to the closed interval `[a, b]` if and only if `a ≤ b`.
|
Set.Ico_inter_Ico
theorem Set.Ico_inter_Ico :
∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
Set.Ico a₁ b₁ ∩ Set.Ico a₂ b₂ = Set.Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
The theorem `Set.Ico_inter_Ico` states that for any type `α` that has a linear order, given any four elements `a₁`, `a₂`, `b₁`, `b₂` of this type `α`, the intersection of the left-closed right-open interval from `a₁` to `b₁` and the left-closed right-open interval from `a₂` to `b₂` is the left-closed right-open interval from the supremum of `a₁` and `a₂` to the infimum of `b₁` and `b₂`. In mathematical terms, it says that $[a₁, b₁) \cap [a₂, b₂) = [max(a₁, a₂), min(b₁, b₂))$ for any $a₁, a₂, b₁, b₂$ in an ordered set.
More concisely: For any ordered type `α` and elements `a₁`, `a₂`, `b₁`, `b₂` in `α`, the intersection of the intervals `[a₁, b₁)` and `[a₂, b₂)` is equal to the interval `[sup a₁ a₂, inf b₁ b₂)`.
|
Set.right_mem_Iic
theorem Set.right_mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∈ Set.Iic a
The theorem `Set.right_mem_Iic` asserts that for any type `α` that has a preorder structure, every element `a` of this type is a member of the left-infinite right-closed interval `Set.Iic a`. In other words, `a` is always less than or equal to `a` itself in this ordered type, which is the definition of the interval `Set.Iic a`.
More concisely: For any type `α` with a preorder structure, every element `a` belongs to the left-infinite right-closed interval `Iic a`.
|
Set.Ico_subset_Ico_right
theorem Set.Ico_subset_Ico_right :
∀ {α : Type u_1} [inst : Preorder α] {a b₁ b₂ : α}, b₁ ≤ b₂ → Set.Ico a b₁ ⊆ Set.Ico a b₂
This theorem states that for any type `α` that has an established preorder (a binary relation that is reflexive and transitive), and any three elements `a`, `b₁`, and `b₂` from this type, if `b₁` is less than or equal to `b₂`, then the left-closed right-open interval from `a` to `b₁` is a subset of the left-closed right-open interval from `a` to `b₂`. In other words, if we have an interval starting at `a` and ending just before `b₂`, and another interval starting at the same point `a` but ending just before `b₁` which is less than or equal to `b₂`, then every element in the second interval is also in the first interval.
More concisely: For any type `α` with a preorder and elements `a`, `b₁`, and `b₂` such that `b₁ ≤ b₂`, the left-closed right-open interval `[a, b₁) is a subset of [a, b₂)`.
|
Set.Ico_eq_empty
theorem Set.Ico_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a < b → Set.Ico a b = ∅
The theorem `Set.Ico_eq_empty` states that for any type `α` equipped with a preorder relation, for any two elements `a` and `b` of `α`, if `a` is not less than `b`, then the left-closed right-open interval from `a` to `b` (represented by `Set.Ico a b`) is empty. In other words, if `a` is not strictly less than `b`, there are no elements `x` such that `a ≤ x` and `x < b`.
More concisely: For any type `α` with a preorder relation, if `a` is not less than `b`, then the interval `[a, b)` is empty.
|
Set.Ico_subset_Icc_self
theorem Set.Ico_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico a b ⊆ Set.Icc a b
This theorem states that for any type `α` that has a preorder, and any two elements `a` and `b` of type `α`, the left-closed right-open interval from `a` to `b` (denoted as `Set.Ico a b`) is a subset of the left-closed right-closed interval from `a` to `b` (denoted as `Set.Icc a b`). In other words, any element that is in the interval `[a, b)` is also in the interval `[a, b]`.
More concisely: For any preorder type `α` and elements `a` and `b` of `α`, the left-closed right-open interval `Set.Ico a b` is a subset of the left-closed right-closed interval `Set.Icc a b`. In other words, `a ≤ x ≤ b` implies `a ≤ x ≤ b` for all `x` in `α`.
|
Set.Ico_subset_Ico
theorem Set.Ico_subset_Ico :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ := by
sorry
This theorem, `Set.Ico_subset_Ico`, states that for any type `α` that has a preorder relation defined on it, given any four elements `a₁`, `a₂`, `b₁`, and `b₂` of this type, if `a₂` is less than or equal to `a₁` and `b₁` is less than or equal to `b₂`, then the left-closed right-open interval from `a₁` to `b₁` is a subset of the left-closed right-open interval from `a₂` to `b₂`. In mathematical terms, if $a₂ \leq a₁$ and $b₁ \leq b₂$, then the set $\{x \,|\, a₁ \leq x < b₁\}$ is included in the set $\{x \,|\, a₂ \leq x < b₂\}$.
More concisely: For any type `α` with a preorder relation, if `a₁ ≤ a₂` and `b₁ ≤ b₂`, then the interval `[a₁, b₁) is subset of [a₂, b₂)`.
|
Set.Iic_top
theorem Set.Iic_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], Set.Iic ⊤ = Set.univ
This theorem states that for any type `α` that has a preorder and a top order (an order where there is a greatest element), the left-infinite right-closed interval `Set.Iic ⊤` (which is the set of all elements that are less than or equal to the greatest element in the type) is equal to the universal set `Set.univ` (the set containing all elements of `α`). In terms of mathematical language, it means that for any set with a preorder and a greatest element ⊤, the interval (-∞, ⊤] corresponds to the whole set.
More concisely: For any type with a preorder and a top element, the left-open, right-closed interval [bottom, top] equals the universal set. (Here, bottom denotes the least element in the preorder, which may or may not exist, and top denotes the greatest element.)
|
Set.Iic_subset_Iic
theorem Set.Iic_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊆ Set.Iic b ↔ a ≤ b
The theorem `Set.Iic_subset_Iic` states that for any type `α` equipped with a preorder, and any two elements `a` and `b` of this type, the left-infinite right-closed interval up to `a` is a subset of the left-infinite right-closed interval up to `b` if and only if `a` is less than or equal to `b`. In other words, all elements less than or equal to `a` are also less than or equal to `b` if and only if `a ≤ b`. This theorem is a fundamental property of ordered sets.
More concisely: For any preordered type `α` and elements `a` and `b`, the left-infinite right-closed interval `{ x : α | x ≤ a }` is subset of the left-infinite right-closed interval `{ x : α | x ≤ b }` if and only if `a ≤ b`.
|
Set.Icc_diff_right
theorem Set.Icc_diff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {b} = Set.Ico a b := by
sorry
This theorem, `Set.Icc_diff_right`, states that for all types `α`, given that `α` has a partial order structure and given any two elements `a` and `b` in `α`, the difference between the left-closed right-closed interval from `a` to `b` and the set containing only `b` equals the left-closed right-open interval from `a` to `b`. In other words, if you take the closed interval `[a, b]` and remove the endpoint `b`, you get the half-open interval `[a, b)`.
More concisely: For all types `α` with a partial order structure, the difference between the left-closed right-closed interval `[a, b]` and the singleton set `{b}` is equal to the left-closed right-open interval `[a, b)` for any `a` and `b` in `α`.
|
Set.Ioc_union_Ioc
theorem Set.Ioc_union_Ioc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
min a b ≤ max c d → min c d ≤ max a b → Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (min a c) (max b d)
The theorem `Set.Ioc_union_Ioc` describes a property of unions of left-open right-closed intervals in any linearly ordered set. Specifically, given any four elements `a`, `b`, `c`, `d` of such a set, if the minimum of `a` and `b` is less than or equal to the maximum of `c` and `d`, and the minimum of `c` and `d` is less than or equal to the maximum of `a` and `b`, then the union of the intervals `(a, b]` and `(c, d]` equals the interval `(min(a, c), max(b, d)]`. This is essentially a statement about the union of overlapping or adjacent intervals in a linear order.
More concisely: If `a ≤ b` and `c ≤ d` in a linearly ordered set, then `(a, b] ∪ (c, d] = (min a c, max b d)`.
|
Set.Ioo_union_left
theorem Set.Ioo_union_left :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → Set.Ioo a b ∪ {a} = Set.Ico a b
This theorem states that for any partially ordered set `α` and any two elements `a` and `b` from that set such that `a` is less than `b`, the union of the open interval `(a, b)` (i.e., set of all `x` in `α` such that `a < x < b`) and the singleton set containing `a` is equivalent to the closed-open interval `[a, b)` (i.e., set of all `x` in `α` such that `a ≤ x < b`). In set theory notation, this can be expressed as `(a, b) ∪ {a} = [a, b)`.
More concisely: For any partially ordered set `α` and elements `a < b` in `α`, the sets `(a, b) ∪ {a}` and `[a, b)` are equal.
|
Set.mem_Icc
theorem Set.mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
The theorem `Set.mem_Icc` states that for any type `α` that has a preorder (a binary relation that is reflexive and transitive), and any elements `a`, `b`, and `x` of `α`, `x` is in the interval from `a` to `b` (including both `a` and `b`) if and only if `x` is greater than or equal to `a` and less than or equal to `b`. In other words, `x` belongs to the closed interval `[a, b]` precisely when `a ≤ x ≤ b`.
More concisely: For any preorder relation on type `α`, an element `x` lies in the interval `[a, b]` if and only if `a ≤ x ≤ b`.
|
Set.Icc_diff_both
theorem Set.Icc_diff_both : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a, b} = Set.Ioo a b := by
sorry
This theorem state that for any given type `α` which has a partial order, and any two elements `a` and `b` of that type, the set difference between the left-closed right-closed interval from `a` to `b` and the set containing `a` and `b` equals the left-open right-open interval from `a` to `b`. In other terms, if you take the closed interval [`a`, `b`] and remove the end points `a` and `b`, you are left with the open interval (`a`, `b`).
More concisely: For any type `α` with a partial order and any `a` and `b` in `α`, the closed interval [`a`, `b`] without `a` and `b` equals the open interval (`a`, `b`).
|
Set.mem_Ioi
theorem Set.mem_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a x : α}, x ∈ Set.Ioi a ↔ a < x
The theorem `Set.mem_Ioi` states that for any type `α` equipped with a preorder, and for any elements `a` and `x` of this type, `x` belongs to the interval `(a, +∞)` (denoted `Set.Ioi a` in Lean), if and only if `a` is strictly less than `x`. This sets up a correspondence between the membership of `x` in the interval `(a, +∞)` and the inequality `a < x`. This interval is a left-open right-infinite interval, meaning it includes all the elements greater than `a` but not `a` itself.
More concisely: For any preordered type `α` and elements `a` and `x` of `α`, `x` belongs to the left-open right-infinite interval `(a, +∞)` if and only if `a` is strictly less than `x`.
|
Set.Iio_subset_Iio
theorem Set.Iio_subset_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Iio a ⊆ Set.Iio b
This theorem states that if `a` is less than or equal to `b` in a given preorder `α`, then the left-infinite right-open interval `(-∞, a)` is a subset of the interval `(-∞, b)`. In other words, if a number is strictly less than `a`, it will also be strictly less than `b` if `a ≤ b`. For linear orders, you should use the theorem `Iio_subset_Iio_iff` for the equivalent condition.
More concisely: If `a ≤ b` holds in a preorder `α`, then `(-∞, a) ⊆ (-∞, b)`.
|
Set.Ioc_subset_Ioc
theorem Set.Ioc_subset_Ioc :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂ := by
sorry
The theorem `Set.Ioc_subset_Ioc` states that for any type `α` that has a preorder structure, and any four elements `a₁`, `a₂`, `b₁`, `b₂` of this type, if `a₂` is less than or equal to `a₁`, and `b₁` is less than or equal to `b₂`, then the left-open right-closed interval from `a₁` to `b₁` is a subset of the left-open right-closed interval from `a₂` to `b₂`. In other words, if we have two intervals such that the second interval starts no later and ends no sooner than the first interval, then all points in the first interval are also in the second interval.
More concisely: For any type `α` with a preorder structure, and any `a₁ ≤ a₂` and `b₁ ≤ b₂` in `α`, the interval `[a₁, b₁) ⊆ [a₂, b₂)`.
|
Set.Iic_union_Ici
theorem Set.Iic_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iic a ∪ Set.Ici a = Set.univ := by
sorry
The theorem `Set.Iic_union_Ici` states that for any type `α` that has a linear order and any element `a` of type `α`, the union of the set of all elements that are less than or equal to `a` (`Set.Iic a`) and the set of all elements that are greater than or equal to `a` (`Set.Ici a`) is the universal set (`Set.univ`). This means that every element in `α` is either less than or equal to `a`, or greater than or equal to `a`, which covers the entirety of `α`.
More concisely: For any linearly ordered type `α` and element `a` in `α`, `Set.Iic a ∪ Set.Ici a = Set.univ`.
|
Set.nonempty_Iic
theorem Set.nonempty_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iic a).Nonempty
This theorem states that for any type `α` with a given preordering, and for any element `a` of this type `α`, the left-infinite right-closed interval `Set.Iic a` is not empty. In simpler terms, it says that there always exists an element in the set of all elements less than or equal to `a`.
More concisely: For any type `α` with a preorder and any element `a` in `α`, the left-infinite right-closed interval `Set.Iic a` is non-empty.
|
Set.Ioi_union_left
theorem Set.Ioi_union_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ioi a ∪ {a} = Set.Ici a
This theorem, named `Set.Ioi_union_left`, states that for any given type `α` with a partial order and any element `a` of this type, the union of the set of all elements strictly greater than `a` (denoted as `Set.Ioi a`) and the singleton set containing `a` is equal to the set of all elements greater than or equal to `a` (denoted as `Set.Ici a`). This essentially tells us that the "open" set of elements greater than `a`, when combined with `a`, forms the "closed" set of elements greater than or equal to `a`.
More concisely: For any type with a partial order, the union of the upward-closed set containing a single element `a` and the set of elements strictly greater than `a` equals the set of elements greater than or equal to `a`.
|
Set.Iic_union_Ioi
theorem Set.Iic_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iic a ∪ Set.Ioi a = Set.univ := by
sorry
The theorem `Set.Iic_union_Ioi` states that for any type `α` equipped with a linear order and any element `a` of `α`, the union of the left-infinite right-closed interval up to `a` and the left-open right-infinite interval from `a` equals the universal set of `α`. In other words, combining the set of all elements less than or equal to `a` with the set of all elements strictly greater than `a` yields the entire set of elements in `α`.
More concisely: For any type `α` with a linear order, the union of the left-closed, right-unbounded interval `[min α, a]` and the left-open, right-unbounded interval `(a, max α)` equals the entire set `α`.
|
Set.Icc_bot_top
theorem Set.Icc_bot_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α], Set.Icc ⊥ ⊤ = Set.univ
This theorem states that for any type `α` equipped with a partial order and a bounded order, the closed interval from the bottom element `⊥` to the top element `⊥` is equal to the universal set. In other words, every element of the type `α` lies in the interval `[⊥, ⊤]`, where `⊥` and `⊤` are the least and greatest elements of `α`, respectively. This makes sense as the bounded order guarantees the existence of such least and greatest elements, and the closed interval `[⊥, ⊤]` includes all the elements between and including `⊥` and `⊤`, which covers the entire set.
More concisely: For any type `α` equipped with a bounded order, every element lies in the closed interval `[⊥, ⊤]` where `⊥` and `⊤` are the least and greatest elements of `α`.
|
Set.Ico_subset_Iio_self
theorem Set.Ico_subset_Iio_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico a b ⊆ Set.Iio b
The theorem `Set.Ico_subset_Iio_self` states that for any type `α` equipped with a preorder, and any two elements `a` and `b` of type `α`, the left-closed right-open interval from `a` to `b`, denoted `Set.Ico a b`, is a subset of the left-infinite right-open interval ending at `b`, denoted `Set.Iio b`. In other words, all elements `x` satisfying `a ≤ x < b` are also elements satisfying `x < b`.
More concisely: For any preordered type `α` and elements `a < b` in `α`, the left-closed right-open interval `Set.Ico a b` is a subset of the left-infinite right-open interval `Set.Iio b`.
|
Set.nonempty_Ioo
theorem Set.nonempty_Ioo :
∀ {α : Type u_1} [inst : Preorder α] {a b : α} [inst_1 : DenselyOrdered α], (Set.Ioo a b).Nonempty ↔ a < b := by
sorry
This theorem states that for any type `α` with a preorder (i.e., a relation that is reflexive and transitive) and any two elements `a` and `b` of this type, if the type is densely ordered (meaning that for any two distinct elements, there's always another element strictly between them), then the left-open right-open interval between `a` and `b` is nonempty if and only if `a` is less than `b`. Essentially, it asserts that in a densely ordered type, there exist elements in the open interval between `a` and `b` if `a` is less than `b`.
More concisely: In a densely ordered type with preorder relation, an element `a` is strictly less than `b` if and only if the open interval `(a, b)` is nonempty.
|
Set.Ici_diff_left
theorem Set.Ici_diff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ici a \ {a} = Set.Ioi a
This theorem states that for any type `α` that has a `PartialOrder` instance and for any element `a` of type `α`, the set difference of the left-closed right-infinite interval at `a` and the singleton set `{a}` is equal to the left-open right-infinite interval at `a`. In simpler terms, if you have a set of all elements greater than or equal to `a` and you subtract the element `a` from the set, you get the set of all elements strictly greater than `a`. In mathematical notation, this is saying that for all `a`, `[a, ∞) \ {a} = (a, ∞)`.
More concisely: For any type `α` with a `PartialOrder` instance and any `a` in `α`, the set difference of the left-closed right-infinite interval `[a, ∞)` and the singleton set `{a}` equals the left-open right-infinite interval `(a, ∞)`. In other words, `[a, ∞) \ {a} = (a, ∞)`.
|
Set.Ioo_subset_Ioo
theorem Set.Ioo_subset_Ioo :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂ := by
sorry
The theorem `Set.Ioo_subset_Ioo` states that for any type `α` with a preorder, and any four elements `a₁, a₂, b₁, b₂` of `α`, if `a₂` is less than or equal to `a₁`, and `b₁` is less than or equal to `b₂`, then the left-open right-open interval from `a₁` to `b₁` is a subset of the left-open right-open interval from `a₂` to `b₂`. In other words, if we have two intervals (a₁, b₁) and (a₂, b₂), and the left endpoint a₂ of the second interval is less than or equal to the left endpoint a₁ of the first interval, and the right endpoint b₁ of the first interval is less than or equal to the right endpoint b₂ of the second interval, then all the elements of the first interval are also elements of the second interval.
More concisely: For any type `α` with a preorder, and for any `a₁ ≤ a₂` and `b₁ ≤ b₂` in `α`, the interval `(a₁, b₁)` is a subset of `(a₂, b₂)`.
|
Set.Icc_self
theorem Set.Icc_self : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), Set.Icc a a = {a}
This theorem is stating that for any given type `α` which is a partial order, the left-closed and right-closed interval from a value `a` to itself, denoted as `Set.Icc a a`, is simply a set containing the single element `a`. In other words, the interval between a number and itself in a partial order only contains that number.
More concisely: For any partial order type `α`, the interval `Set.Icc a a` consists of exactly the element `a`.
|
Set.Ioo_insert_right
theorem Set.Ioo_insert_right :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → insert b (Set.Ioo a b) = Set.Ioc a b
This theorem states that for any partially ordered set, given two elements `a` and `b` where `a` is less than `b`, the set obtained by inserting `b` into the open interval from `a` to `b` (denoted as `(a, b)`, exclusive of `a` and `b`) is equivalent to the interval from `a` to `b` including `b` (denoted as `(a, b]`). In other words, adding the right endpoint to a left-open right-open interval transforms it into a left-open right-closed interval.
More concisely: For any partially ordered set, the set obtained by inserting an element into a left-open interval is equal to the corresponding left-open right-closed interval.
|
Set.Icc_subset_Icc_iff
theorem Set.Icc_subset_Icc_iff :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α},
a₁ ≤ b₁ → (Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
The theorem `Set.Icc_subset_Icc_iff` is a statement about intervals on a preorder. Specifically, for any type `α` equipped with a preorder, and any four elements `a₁`, `a₂`, `b₁`, `b₂` of `α` such that `a₁` is less than or equal to `b₁`, the interval `[a₁, b₁]` is a subset of the interval `[a₂, b₂]` if and only if `a₂` is less than or equal to `a₁` and `b₁` is less than or equal to `b₂`. Here, `[a, b]` denotes the closed interval from `a` to `b`, i.e., the set of all elements `x` such that `a ≤ x ≤ b`.
More concisely: For any preorder `α` and elements `a₁`, `a₂`, `b₁`, `b₂` in `α` with `a₁ ≤ b₁`, the intervals `[a₁, b₁]` and `[a₂, b₂]` are equal if and only if `a₁ ≤ a₂` and `b₁ ≤ b₂`. (Note: `[a, b]` denotes the closed interval from `a` to `b`.)
|
Set.Iio_subset_Iic
theorem Set.Iio_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Iio a ⊆ Set.Iic b
This theorem states that for any type `α` equipped with a preorder and any `a` and `b` in `α`, if `a` is less than or equal to `b`, then the left-infinite right-open interval `(-∞, a)` is a subset of the left-infinite right-closed interval `(-∞, b]`. In simpler terms, any element that is less than `a` is also less than or equal to `b`. Note that this is only an implication. If you need an equivalence for this statement in the context of dense linear orders, you should use the theorem `Iio_subset_Iic_iff`.
More concisely: For any preorder `α` and `a, b` in `α` with `a ≤ b`, the left-infinite right-open interval `(-∞, a)` is a subset of the left-infinite right-closed interval `(-∞, b]`.
|
Set.Iio_inter_Iio
theorem Set.Iio_inter_Iio :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a ∩ Set.Iio b = Set.Iio (a ⊓ b)
The theorem `Set.Iio_inter_Iio` states that for any type `α` that has a linear order, given any two elements `a` and `b` of the type `α`, the intersection of the left-infinite right-open intervals ending at `a` and `b` respectively, is equal to the left-infinite right-open interval ending at the infimum of `a` and `b` (denoted by `a ⊓ b`). In other words, the intersection of all elements less than `a` and all elements less than `b` is the set of all elements less than the smaller of `a` and `b`.
More concisely: For any linear order type `α`, the interval `{x : α | x < a} ∩ {x : α | x < b} = {x : α | x < a ⊓ b}`, where `a ⊓ b` denotes the infimum of `a` and `b`.
|
Set.nonempty_Ioc
theorem Set.nonempty_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioc a b).Nonempty ↔ a < b
The theorem `Set.nonempty_Ioc` states that for any type `α` with a preorder (a binary relation that is reflexive and transitive) and any two elements `a` and `b` of that type, the interval `(a, b]` (i.e., the set of all elements `x` such that `a < x ≤ b`) is nonempty (i.e., contains at least one element) if and only if `a < b`. This essentially says that an interval `(a, b]` has elements if `a` is strictly less than `b`.
More concisely: For any type with a preorder, the interval (a, b] is nonempty if and only if a < b.
|
Set.Ici_diff_Ioi_same
theorem Set.Ici_diff_Ioi_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Ici a \ Set.Ioi a = {a} := by
sorry
This theorem states that for any type `α` which has a partial order, the set difference between the left-closed right-infinite interval starting from a particular value `a` and the left-open right-infinite interval starting from the same value `a`, is the singleton set containing only `a`. In mathematical terms, it's saying that if you remove from the set of all elements greater than or equal to `a` those strictly greater than `a`, you're left with the set containing only `a`.
More concisely: For any type `α` with a partial order, the left-closed right-infinite interval and the left-open right-infinite interval starting from `a` differ by a singleton set containing only `a`.
|
Set.Ici_subset_Ici
theorem Set.Ici_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊆ Set.Ici b ↔ b ≤ a
This theorem states that for any type `α` that has a preorder, and any two elements `a` and `b` of that type, the left-closed right-infinite interval starting at `a` is a subset of the left-closed right-infinite interval starting at `b` if and only if `b` is less than or equal to `a`. In more mathematical terms, it asserts that for all `a` and `b` in a preordered set, $[a, \infty)$ is contained in $[b, \infty)$ if and only if $b \leq a$.
More concisely: For any preordered type `α`, elements `a` and `b` in `α` satisfy $[a, \infty) \subseteq [b, \infty)$ if and only if `b` is less than or equal to `a`.
|
Set.compl_Iic
theorem Set.compl_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Iic a)ᶜ = Set.Ioi a
This theorem states that for any type `α` that has a linear order, the complement of the set of all elements `x` that are less than or equal to a given element `a` (denoted as `Set.Iic a`), is exactly the set of all elements `x` that are strictly greater than `a` (denoted as `Set.Ioi a`). In mathematical terms, this theorem states that for any `a` in a linearly ordered set `α`, the property `(∀x ∈ α, x ≤ a)^c = ∀x ∈ α, a < x` holds.
More concisely: For any linearly ordered type `α` and element `a` in `α`, the complement of the set of elements less than or equal to `a` is equal to the set of elements strictly greater than `a`. In mathematical notation, `Set.Iic a = Set.Ioi a`.
|
Set.Ico_subset_Ico_union_Ico
theorem Set.Ico_subset_Ico_union_Ico :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
The theorem `Set.Ico_subset_Ico_union_Ico` states that for any linearly ordered type `α` and any three elements `a`, `b`, and `c` of this type, the left-closed right-open interval from `a` to `c` (denoted `Set.Ico a c`) is a subset of the union of the left-closed right-open interval from `a` to `b` and the left-closed right-open interval from `b` to `c` (denoted `Set.Ico a b ∪ Set.Ico b c`). In mathematical terms, we are saying if `x` is in the interval `[a, c)`, then `x` is necessarily in the interval `[a, b)` or in the interval `[b, c)`.
More concisely: For any linearly ordered type `α` and elements `a < b < c` in `α`, `Set.Ico a c` is a subset of `Set.Ico a b ∪ Set.Ico b c`. In other words, every element in the left-closed right-open interval from `a` to `c` belongs to either the interval from `a` to `b` or the interval from `b` to `c`.
|
Set.mem_Iic
theorem Set.mem_Iic : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Iic b ↔ x ≤ b
This theorem, `Set.mem_Iic`, states that for any type `α` that has a preorder, and for any elements `b` and `x` of this type, `x` is an element of the set `Set.Iic b` if and only if `x` is less than or equal to `b`. In other words, it verifies that the set `Set.Iic b` precisely consists of the elements that are less than or equal to `b`.
More concisely: For any preordered type `α` and elements `b` and `x` of `α`, `x` is in `Set.Iic b` if and only if `x ≤ b`.
|
Set.mem_Iio
theorem Set.mem_Iio : ∀ {α : Type u_1} [inst : Preorder α] {b x : α}, x ∈ Set.Iio b ↔ x < b
The theorem `Set.mem_Iio` states that for any type `α` equipped with a preorder, and any elements `b` and `x` of this type, `x` belongs to the left-infinite right-open interval `Set.Iio b` if and only if `x` is less than `b`. In other words, the function `Set.Iio b` is precisely the set of all elements less than `b`.
More concisely: For any preordered type `α` and elements `b` and `x` of `α`, `x` is in the left-infinite right-open interval `Set.Iio b` if and only if `x` is strictly less than `b`.
|
Set.right_mem_Icc
theorem Set.right_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ Set.Icc a b ↔ a ≤ b
This theorem states that for any type `α` that has a preorder structure and for any two elements `a` and `b` of type `α`, `b` is an element of the closed interval from `a` to `b`, denoted `Set.Icc a b`, if and only if `a` is less than or equal to `b`. In other words, the right endpoint `b` of the interval `[a, b]` is part of the interval if `a` is not greater than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` of `α`, `b` belongs to the closed interval `Icc a b` if and only if `a` is less than or equal to `b`.
|
Set.dual_Icc
theorem Set.dual_Icc :
∀ {α : Type u_1} [inst : Preorder α] {a b : α},
Set.Icc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Icc b a
The theorem `Set.dual_Icc` states that for any type `α` with a preorder, and any two elements `a` and `b` of `α`, the closed interval from `a` to `b` in the dual order is the same as the preimage of the closed interval from `b` to `a` under the function `OrderDual.ofDual`. In other words, it asserts the duality between intervals in a preordered set and its dual.
More concisely: For any preordered type `α` and elements `a` and `b` in `α`, the dual interval `[OrderDual.ofDual b, OrderDual.ofDual a]` is equal to the closed interval `[a, b]` in the original order.
|
Set.Ioo_eq_empty_iff
theorem Set.Ioo_eq_empty_iff :
∀ {α : Type u_1} [inst : Preorder α] {a b : α} [inst_1 : DenselyOrdered α], Set.Ioo a b = ∅ ↔ ¬a < b
This theorem states that for any type `α` with a preorder and any two elements `a` and `b` of `α`, under the condition that `α` is densely ordered, the open interval from `a` to `b` (denoted by `Set.Ioo a b`, which includes all elements `x` such that `a < x < b`) is empty if and only if `a` is not less than `b`. In other words, if `a` is not less than `b`, there are no elements `x` between `a` and `b`, hence the open interval is empty. Conversely, if the open interval is empty, this implies that there are no elements between `a` and `b`, hence `a` cannot be less than `b`.
More concisely: For a densely ordered type `α` and elements `a` and `b` of `α`, the open interval `Set.Ioo a b` is empty if and only if `a` is not less than `b`.
|
Set.nonempty_Ioi
theorem Set.nonempty_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [inst_1 : NoMaxOrder α], (Set.Ioi a).Nonempty
The theorem `Set.nonempty_Ioi` states that for any type `α` that has a `Preorder` relationship (which means that it has a binary relation that is reflexive and transitive) and a property of `NoMaxOrder` (which means there is no maximum element), and for any element `a` of type `α`, the set of elements that are greater than `a` (`Set.Ioi a`) is non-empty. In other words, there is always an element in type `α` that is larger than `a`.
More concisely: For any type `α` with a `Preorder` and `NoMaxOrder` relation, the set of elements strictly greater than any given element `a` is non-empty.
|
Set.Ioo_subset_Iio_self
theorem Set.Ioo_subset_Iio_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Iio b
The theorem `Set.Ioo_subset_Iio_self` states that for all types `α` with a preorder, and for all `a` and `b` of type `α`, the set of all elements `x` such that `a` is less than `x` and `x` is less than `b` (denoted as `Set.Ioo a b`) is a subset of the set of all elements `x` such that `x` is less than `b` (denoted as `Set.Iio b`). In mathematical terms, we can say that the open interval $(a, b)$ is a subset of the half-open interval $(-\infty, b)$.
More concisely: For all types `α` with a preorder and all `a` and `b` in `α`, the open interval `Ioo a b` is contained in the half-open interval `Iio b`.
|
Set.Ioi_inter_Iio
theorem Set.Ioi_inter_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iio b = Set.Ioo a b := by
sorry
This theorem states that for any type `α` that has a preorder (a relation that is reflexive and transitive), and any two elements `a` and `b` of that type, the intersection of the set of all elements greater than `a` (denoted as `Set.Ioi a`) and the set of all elements less than `b` (denoted as `Set.Iio b`) is exactly the set of all elements `x` such that `a < x < b` (denoted as `Set.Ioo a b`). In mathematical terms, it can be written as $(a, \infty) \cap (-\infty, b) = (a, b)$.
More concisely: For any type `α` with a preorder, and elements `a` and `b` of `α`, `Set.Ioi a ∩ Set.Iio b` equals `Set.Ioo a b`.
|
Set.Ioc_eq_empty_of_le
theorem Set.Ioc_eq_empty_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ioc a b = ∅
This theorem states that for any type `α` that has a preorder structure, given any two elements `a` and `b` from this type, if `b` is less than or equal to `a`, then the left-open right-closed interval from `a` to `b` is an empty set. In other words, there are no elements `x` such that `x` is greater than `a` and less than or equal to `b`.
More concisely: For any preordered type `α` and elements `a` and `b` with `b ≤ a`, the interval `(a, b]` is empty.
|
Set.Ioi_inter_Iic
theorem Set.Ioi_inter_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iic b = Set.Ioc a b := by
sorry
This theorem states that for any type `α` equipped with a preorder relation, and for any two elements `a` and `b` of this type, the intersection of the set of elements greater than `a` (an open interval on the left) and the set of elements less than or equal to `b` (a closed interval on the right) is exactly the set of elements that are strictly greater than `a` and less than or equal to `b` (a left-open right-closed interval). In other words, $(a, +\infty) \cap (-\infty, b] = (a, b]$.
More concisely: For any preordered type `α` and elements `a` and `b` of `α`, the intersection of the sets of elements strictly greater than `a` and less than or equal to `b` equals the set of elements strictly greater than `a` and less than or equal to `b`. In other words, $(a, \infty) \cap (-\infty, b] = (a, b]$.
|
Set.mem_Ico
theorem Set.mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ico a b ↔ a ≤ x ∧ x < b
The theorem `Set.mem_Ico` states that for any type `α` that has a preorder structure, and for any elements `a`, `b`, and `x` of `α`, `x` belongs to the left-closed right-open interval from `a` to `b` if and only if `x` is greater than or equal to `a` and less than `b`. In other words, a membership of `x` in the interval `[a, b)` (denoted as `Set.Ico a b` in Lean) is characterized by the inequalities `a ≤ x < b`.
More concisely: For any preordered type `α` and elements `a`, `b` of `α`, an element `x` belongs to the left-closed right-open interval `[a, b)` if and only if `a ≤ x < b`.
|
Set.Iic_injective
theorem Set.Iic_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective Set.Iic
The theorem `Set.Iic_injective` states that for any type `α` where a partial order is defined, the function `Set.Iic`, which produces the left-infinite right-closed interval `{x | x ≤ b}`, is injective. In other words, if two such intervals are equal, then their endpoints must be the same. This means that for all elements `a₁`, `a₂` of the type `α`, if `Set.Iic a₁` equals `Set.Iic a₂`, then `a₁` equals `a₂`.
More concisely: For any type `α` with a partial order, the function `Set.Iic` mapping an element to its left-infinite right-closed interval is injective. In other words, for all `α` elements `a₁` and `a₂`, if `Set.Iic a₁ = Set.Iic a₂`, then `a₁ = a₂`.
|
Set.Ioc_subset_Ioc_union_Ioc
theorem Set.Ioc_subset_Ioc_union_Ioc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a c ⊆ Set.Ioc a b ∪ Set.Ioc b c
This theorem states that for any linearly ordered type `α` and any three elements `a`, `b`, and `c` of `α`, the left-open right-closed interval from `a` to `c` is a subset of the union of the left-open right-closed interval from `a` to `b` and the left-open right-closed interval from `b` to `c`. In mathematical terms, it states that for all `a`, `b`, and `c` in a linear order, the interval `(a, c]` is contained within the union of the intervals `(a, b]` and `(b, c]`.
More concisely: For any linearly ordered type `α` and elements `a`, `b`, `c` in `α` with `a < b < c`, the left-open right-closed interval `(a, c]` is a subset of the union of `(a, b]` and `(b, c]`.
|
Set.Ici_inter_Iio
theorem Set.Ici_inter_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ∩ Set.Iio b = Set.Ico a b := by
sorry
This theorem states that for any type `α` with a preorder structure, and any two elements `a` and `b` of `α`, the intersection of the left-closed right-infinite interval starting at `a` (`Set.Ici a`) and the left-infinite right-open interval ending at `b` (`Set.Iio b`) is equal to the left-closed right-open interval from `a` to `b` (`Set.Ico a b`). In other words, the set of all elements `x` such that `x` is greater than or equal to `a` and less than `b` can be obtained by taking the intersection of the set of all elements greater than or equal to `a` and the set of all elements less than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` in `α`, the interval from `a` to `b` (left-closed and right-open) is equal to the intersection of the left-closed right-infinite interval starting at `a` and the left-infinite right-open interval ending at `b`.
|
Set.Icc_inter_Icc
theorem Set.Icc_inter_Icc :
∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
Set.Icc a₁ b₁ ∩ Set.Icc a₂ b₂ = Set.Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
This theorem states that for any lattice structure α, and any four elements `a₁`, `a₂`, `b₁`, `b₂` of α, the intersection of the closed interval from `a₁` to `b₁` and the closed interval from `a₂` to `b₂` is equal to the closed interval from the supremum (`⊔`) of `a₁` and `a₂` to the infimum (`⊓`) of `b₁` and `b₂`. In other words, when two closed intervals on a lattice intersect, the resulting set is also a closed interval whose lower bound is the larger of the two original lower bounds and whose upper bound is the smaller of the two original upper bounds.
More concisely: For any lattice α and elements a₁, a₂, b₁, b₂, the intersection of the closed intervals [a₁, b₁] and [a₂, b₂] is equal to the closed interval [⊔(a₁, a₂), ⊓(b₁, b₂)], where ⊔ and ⊓ denote the lattice supremum and infimum, respectively.
|
Set.dual_Ico
theorem Set.dual_Ico :
∀ {α : Type u_1} [inst : Preorder α] {a b : α},
Set.Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioc b a
The theorem `Set.dual_Ico` states that for any type `α` with a preorder and any pair of elements `a` and `b` of `α`, the left-closed right-open interval (`Set.Ico`) between the order duals of `a` and `b` is equivalent to the preimage of the left-open right-closed interval (`Set.Ioc`) between `b` and `a` under the function that converts an order dual back to an original order. In other words, it states that reversing the order of a preorder results in swapping the roles of the open and closed ends of an interval.
More concisely: For any preordered type `α` and elements `a` and `b` in `α`, the left-closed right-open interval `Set.Ico a b` is equivalent to the preimage of the left-open right-closed interval `Set.Ioc b a` under the order dual function.
|
Set.Icc_subset_Ici_self
theorem Set.Icc_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b ⊆ Set.Ici a
The theorem `Set.Icc_subset_Ici_self` states that for any type `α` with a preorder structure, any left-closed right-closed interval `[a, b]` (that is, the set of all `x` such that `a ≤ x` and `x ≤ b`) is a subset of the left-closed right-infinite interval starting at `a` (that is, the set of all `x` such that `a ≤ x`). This is intuitively true since any element in the interval `[a, b]` will certainly be greater than or equal to `a`.
More concisely: For any preordered type `α` and elements `a ≤ b` in `α`, the interval `[a, b]` is a subset of the interval `{x : α | a ≤ x}`.
|
Set.Icc_subset_Icc
theorem Set.Icc_subset_Icc :
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ ≤ a₁ → b₁ ≤ b₂ → Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ := by
sorry
The theorem `Set.Icc_subset_Icc` states that for any type `α` that has a preorder (a binary relation that is reflexive and transitive), and for any four elements `a₁`, `a₂`, `b₁`, `b₂` of this type, if `a₂` is less than or equal to `a₁` and `b₁` is less than or equal to `b₂`, then the closed interval from `a₁` to `b₁` is a subset of the closed interval from `a₂` to `b₂`. In other words, if we increase the lower bound and decrease the upper bound of an interval, then the resulting interval is a subset of the original one.
More concisely: For any type `α` with a preorder and `a₁ ≤ a₂` and `b₁ ≤ b₂`, the interval `[a₁, b₁]` is a subset of the interval `[a₂, b₂]`.
|
Set.Icc_diff_Ioo_same
theorem Set.Icc_diff_Ioo_same :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Icc a b \ Set.Ioo a b = {a, b}
The theorem `Set.Icc_diff_Ioo_same` states that for any type `α` that is ordered with a partial order, given any two elements `a` and `b` from `α` such that `a` is less than or equal to `b`, the difference between the closed interval [a, b] and the open interval (a, b) is the set containing only the elements `a` and `b`. In terms of mathematics, this corresponds to the following set difference: `[a, b] \ (a, b) = {a, b}`.
More concisely: For any ordered type `α` and elements `a ≤ b` in `α`, the set difference between the closed interval `[a, b]` and the open interval `(a, b)` equals the singleton set `{a, b}`.
|
Set.Iic_subset_Iio
theorem Set.Iic_subset_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊆ Set.Iio b ↔ a < b
The theorem `Set.Iic_subset_Iio` states that for any type `α` with a preorder relation, and any two elements `a` and `b` of this type, the set of all elements less than or equal to `a` (`Set.Iic a`) is a subset of the set of all elements strictly less than `b` (`Set.Iio b`) if and only if `a` is strictly less than `b`. In other words, all elements less than or equal to `a` are also strictly less than `b` if and only if `a` is strictly less than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` of `α`, `Set.Iic a ⊆ Set.Iio b` if and only if `a` is strictly less than `b`.
|
Set.Ioi_subset_Ioi
theorem Set.Ioi_subset_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Ioi b ⊆ Set.Ioi a
This theorem states that, for any type `α` with a preorder structure (a structure in which elements can be compared as less than, equal, or greater than), if we have two elements `a` and `b` such that `a` is less than or equal to `b`, then the open, right-infinite interval starting from `b` is a subset of the open, right-infinite interval starting from `a`. In simpler terms, if `a` is not strictly greater than `b`, then all the elements strictly greater than `b` are also strictly greater than `a`. This is a simple implication in preorders. If you want the equivalent statement in linear orders, use the theorem `Ioi_subset_Ioi_iff`.
More concisely: For any preorder `α`, if `a ≤ b` then the open right-interval `(b : α) ^+ := {x : α | ∃ (h : ℕ), x = a + h} ` is a subset of the open right-interval `(b : α) ^+ := {x : α | ∃ (h : ℕ), x = b + h} `.
|
Set.mem_Icc_of_Ico
theorem Set.mem_Icc_of_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ico a b → x ∈ Set.Icc a b := by
sorry
The theorem `Set.mem_Icc_of_Ico` states that for any type `α` that has a preorder relation (`≤`), and any three elements `a`, `b`, and `x` of type `α`, if `x` belongs to the left-closed right-open interval from `a` to `b` (denoted `Set.Ico a b`), then `x` also belongs to the left-closed right-closed interval from `a` to `b` (denoted `Set.Icc a b`). In mathematical terms, if `a ≤ x < b`, then it's also true that `a ≤ x ≤ b`.
More concisely: If `a ≤ x` and `x < b` hold in a preordered type `α`, then `a ≤ x ≤ b`. In other words, every left-closed right-open interval is a subset of the corresponding left-closed right-closed interval.
|
Set.Icc_eq_empty_of_lt
theorem Set.Icc_eq_empty_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → Set.Icc a b = ∅
This theorem states that for any type `α` that has a `Preorder` (an algebraic structure that captures the intuitive notion of an ordering that can be "less than", "equal to", or "greater than"), if `b` is less than `a`, then the closed interval from `a` to `b` (inclusive), denoted `Set.Icc a b`, is empty. In other words, there are no elements `x` in `α` such that `a ≤ x ≤ b` when `b < a`.
More concisely: For any preordered type `α`, the closed interval `Set.Icc a b` is empty when `b` is strictly less than `a`.
|
Set.Iio_subset_Iic_self
theorem Set.Iio_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a ⊆ Set.Iic a
The theorem `Set.Iio_subset_Iic_self` states that for any type `α` that has a preorder relation, and for any element `a` of that type, the left-infinite right-open interval up to `a` is a subset of the left-infinite right-closed interval up to `a`. In mathematical terms, this means that for all `x` in `α`, if `x` is less than `a`, then `x` is also less than or equal to `a`.
More concisely: For any type `α` with a preorder relation and any element `a` in `α`, the left-infinite right-open interval `(−∞, a)` is a subset of the left-infinite right-closed interval `[−∞, a]`.
|
Set.right_mem_Ioc
theorem Set.right_mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ Set.Ioc a b ↔ a < b
This theorem states that for any type `α` that has a predefined `Preorder` relation, and for any two elements `a` and `b` of this type, `b` is an element of the left-open, right-closed interval between `a` and `b` if and only if `a` is less than `b`. In mathematical terms, for a ≤-preordered set α and elements a, b ∈ α, b belongs to the interval (a, b] if and only if a < b.
More concisely: For any preordered set (α, ≤) and elements a, b in α, b lies in the left-open, right-closed interval (a, b] if and only if a < b.
|
Set.compl_Iio
theorem Set.compl_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Iio a)ᶜ = Set.Ici a
This theorem, `Set.compl_Iio`, states that for any type `α` that has an instance of linear order, and for any element `a` of type `α`, the complement of the left-infinite, right-open interval ending at `a` is equal to the left-closed, right-infinite interval starting from `a`. In other words, every element not less than `a` (the complement of all elements less than `a`) is either equal to `a` or greater than `a`.
More concisely: For any type `α` with a linear order and any `a` in `α`, the complement of the left-open, right-infinite interval `(−∞, a)` is equal to the left-closed, right-infinite interval `[a, +∞)`.
|
Set.Ioc_inter_Ioc
theorem Set.Ioc_inter_Ioc :
∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
Set.Ioc a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
This theorem states that for any type `α` with a linear order, given four elements `a₁`, `a₂`, `b₁`, and `b₂` of this type, the intersection of the interval `(a₁, b₁]` and the interval `(a₂, b₂]` is the interval `(max{a₁, a₂}, min{b₁, b₂}]`. Here, `(a, b]` denotes the set of elements `x` such that `a < x` and `x ≤ b`. The notation `a₁ ⊔ a₂` represents the maximum of `a₁` and `a₂`, and `b₁ ⊓ b₂` represents the minimum of `b₁` and `b₂`.
More concisely: For any type `α` with a linear order, the intersection of the intervals `(a₁, b₁]` and `(a₂, b₂]` is equal to `(max{a₁, a₂}, min{b₁, b₂}]`.
|
Set.nonempty_Ico
theorem Set.nonempty_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ico a b).Nonempty ↔ a < b
The theorem `Set.nonempty_Ico` states that for any type `α` that has a preorder relationship, and any two elements `a` and `b` of type `α`, the left-closed right-open interval `(Set.Ico a b)` is nonempty if and only if `a` is less than `b`. In other words, there exists an element in the interval from `a` to `b`, not including `b`, if and only if `a` is strictly less than `b`.
More concisely: The set of elements between `a` and `b` (inclusive of `a` but exclusive of `b`) in a preordered type `α` is nonempty if and only if `a` is strictly less than `b`.
|
Set.Ioc_union_left
theorem Set.Ioc_union_left :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Ioc a b ∪ {a} = Set.Icc a b
This theorem states that for any partially ordered type `α` and any two elements `a` and `b` of `α` where `a` is less than or equal to `b`, the union of the left-open right-closed interval from `a` to `b` (`Set.Ioc a b`) and the singleton set containing `a` is equal to the left-closed right-closed interval from `a` to `b` (`Set.Icc a b`). In other words, if we add the left endpoint `a` to the interval `(a, b]`, we get the interval `[a, b]`.
More concisely: For any partially ordered type `α` and elements `a` and `b` in `α` with `a ≤ b`, `Set.Ioc a b ∪ {a} = Set.Icc a b`.
|
Set.Ici_injective
theorem Set.Ici_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective Set.Ici
This theorem states that for all types `α` that have a `PartialOrder` instance, the function `Set.Ici` is injective. In other words, if we have two elements `a` and `b` of type `α`, and the left-closed right-infinite interval starting from `a` is the same as the one starting from `b` (i.e., all elements greater than or equal to `a` are the same as those greater than or equal to `b`), then `a` must be equal to `b`. This is essentially saying that each distinct point defines a unique left-closed right-infinite interval in a partially ordered set.
More concisely: If `α` is a type with a `PartialOrder` instance, then the function `Set.Ici` mapping an element `x` to the left-closed right-infinite interval `{ y | y ≥ x }` is an injection.
|
IsMax.Ici_eq
theorem IsMax.Ici_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, IsMax a → Set.Ici a = {a}
The theorem `IsMax.Ici_eq` states that for any partially ordered type `α` and any element `a` of that type, if `a` is a maximal element (meaning that no other element is strictly greater than `a`), then the set of all elements that are greater than or equal to `a` (denoted by `Set.Ici a`) is simply the set containing the element `a` itself. In other words, there are no elements in the set that are strictly greater than `a`, so the only element in the set is `a`.
More concisely: For any partially ordered type `α` and its maximal element `a`, the set of elements greater than or equal to `a` (`Set.Ici a`) equals the singleton set `{a}` if `a` is maximal.
|
Set.nonempty_Icc
theorem Set.nonempty_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Icc a b).Nonempty ↔ a ≤ b
This theorem, `Set.nonempty_Icc`, states that for any type `α` (denoted by `{α : Type u_1}`) equipped with a preorder (denoted by `[inst : Preorder α]`), and any two elements `a` and `b` of type `α` (denoted by `{a b : α}`), the left-closed and right-closed interval from `a` to `b` (expressed as `Set.Icc a b`) is nonempty if and only if `a` is less than or equal to `b`. In other words, there exists at least one element in the interval `[a, b]` if `a ≤ b`.
More concisely: For any type `α` with preorder and any `a, b ∈ α`, the interval `Icc a b` is nonempty if and only if `a ≤ b`.
|
Set.compl_Ici
theorem Set.compl_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Ici a)ᶜ = Set.Iio a
The theorem `Set.compl_Ici` states that for any type `α` with a linear order and any element `a` of that type, the complement of the set of elements that are greater than or equal to `a` (notated as `(Set.Ici a)ᶜ`) is exactly the set of elements that are strictly less than `a` (notated as `Set.Iio a`). In other words, it asserts that the elements not in a left-closed right-infinite interval starting at `a` are precisely those in a left-infinite right-open interval ending just before `a`.
More concisely: The complement of the left-closed right-infinite interval `(Set.Ici a)` equals the left-infinite right-open interval `Set.Iio a`.
|
Set.Ioi_subset_Ici
theorem Set.Ioi_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → Set.Ioi b ⊆ Set.Ici a
The theorem states that for any type `α` with a preorder structure, and any two elements `a` and `b` of `α`, if `a` is less than or equal to `b`, then the interval `(b, +∞)` is a subset of the interval `[a, +∞)`. In other words, all elements greater than `b` are also greater than or equal to `a`. This is straightforward for preorders, but if the relation is a dense linear order, a different theorem `Ioi_subset_Ici_iff` should be used.
More concisely: For any preorder `α`, if `a ≤ b` in `α`, then the interval `(b, +∞) ⊆ [a, +∞)`.
|
Set.nonempty_Iio
theorem Set.nonempty_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [inst_1 : NoMinOrder α], (Set.Iio a).Nonempty
This theorem, `Set.nonempty_Iio`, states that for any type `α` equipped with a preorder and a property that it does not have a minimal element (`NoMinOrder`), the left-infinite right-open interval `(Set.Iio a)` is nonempty. In other words, there always exists an element `x` in the type `α` such that `x` is less than `a`. This is expressed using the property `Set.Nonempty` which is a way of stating that a set is not empty.
More concisely: If `α` is a type equipped with a preorder and has no minimal element, then the left-infinite right-open interval `(Set.Iio a)` of `α` is nonempty.
|
Set.Icc_diff_left
theorem Set.Icc_diff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Icc a b \ {a} = Set.Ioc a b := by
sorry
This theorem states that for any partial order set `α` and any two elements `a` and `b` in this set, the difference between the closed interval (including both endpoints) `[a, b]` and the singleton set `{a}` is equal to the half-open interval `(a, b]`. In other words, if you start with the closed interval `[a, b]` and remove the point `a`, you end up with the half-open interval `(a, b]`, which includes `b` but not `a`.
More concisely: For any partial order set `α`, the difference between the closed interval `[a, b]` and the singleton set `{a}` is equal to the half-open interval `(a, b]`. In other words, `[a, b] \ {a} = (a, b]`.
|
Set.nonempty_Ici
theorem Set.nonempty_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ici a).Nonempty
The theorem `Set.nonempty_Ici` states that for every type `α` that has a preorder structure, and for any element `a` of this type `α`, the left-closed right-infinite interval `Set.Ici a` is nonempty. In terms of mathematics, for any value `a`, there always exists at least one element `x` such that `a` is less than or equal to `x` (i.e., `a ≤ x`) within the given set.
More concisely: For any preordered type `α` and element `a` in `α`, the left-closed right-infinite interval `Ici a` is nonempty, containing some element `x` with `a ≤ x`.
|
Set.Ioo_subset_Ioc_self
theorem Set.Ioo_subset_Ioc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Ioc a b
The theorem `Set.Ioo_subset_Ioc_self` states that for all types `α` with a preorder (an order relation that is reflexive and transitive), and for all elements `a` and `b` of type `α`, the set of elements `x` such that `a` is less than `x` and `x` is less than `b` (denoted as `Set.Ioo a b`, or the open interval (a, b)) is a subset of the set of elements `x` such that `a` is less than `x` and `x` is less than or equal to `b` (denoted as `Set.Ioc a b`, or the half-open interval (a, b]). This means that every element in the open interval (a, b) is also present in the half-open interval (a, b].
More concisely: The open interval (a, b) is a subset of the half-open interval (a, b] for all elements a and b of a preordered type α.
|
Set.Ioc_diff_right
theorem Set.Ioc_diff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ioc a b \ {b} = Set.Ioo a b := by
sorry
The theorem `Set.Ioc_diff_right` states that for any type `α` which has a `PartialOrder` instance and any two elements `a` and `b` of this type, the difference between the left-open right-closed interval from `a` to `b` and the singleton set `{b}` is equal to the left-open right-open interval from `a` to `b`. In other words, if you remove the right endpoint `b` from the interval `(a, b]`, you get the open interval `(a, b)`.
More concisely: For any type `α` with a `PartialOrder` structure and elements `a` and `b` of `α`, the interval `(a, b]` (left-open right-closed) equals the set difference between `(a, b)` (left-open right-open) and the singleton set `{b}`.
|
Set.mem_Ici
theorem Set.mem_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a x : α}, x ∈ Set.Ici a ↔ a ≤ x
The theorem `Set.mem_Ici` states that for any type `α` with a preorder and any elements `a` and `x` of `α`, `x` belongs to the left-closed right-infinite interval starting at `a` if and only if `a` is less than or equal to `x`. In other words, this theorem describes the condition for a value `x` to be in the interval that starts at `a` and includes all values greater than or equal to `a`.
More concisely: For any preordered type `α` and elements `a` and `x` of `α`, `x` belongs to the left-closed right-infinite interval starting at `a` if and only if `a` is less than or equal to `x`.
|
Set.Icc_subset_Iic_self
theorem Set.Icc_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc a b ⊆ Set.Iic b
This theorem states that for any type `α` that has a preorder structure, and for any two elements `a` and `b` of this type, the left-closed right-closed interval from `a` to `b` (denoted as `Set.Icc a b`, including all `x` such that `a ≤ x ≤ b`) is a subset of the left-infinite right-closed interval ending at `b` (denoted as `Set.Iic b`, including all `x` such that `x ≤ b`).
More concisely: For any preorder type `α` and elements `a ≤ b` in `α`, the left-closed right-closed interval `Set.Icc a b` is a subset of the left-infinite right-closed interval `Set.Iic b`.
|
Set.Ici_inter_Ici
theorem Set.Ici_inter_Ici :
∀ {α : Type u_1} [inst : SemilatticeSup α] {a b : α}, Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)
The theorem `Set.Ici_inter_Ici` states that for any type `α` that is a semilattice with a supremum operation (`⊔`), and for any elements `a` and `b` of this type, the intersection of the interval of elements greater than or equal to `a` (`Set.Ici a`) and the interval of elements greater than or equal to `b` (`Set.Ici b`) is equal to the interval of elements greater than or equal to the supremum of `a` and `b` (`Set.Ici (a ⊔ b)`). This means, in more natural terms, that when we take the overlap of all elements larger than `a` and all elements larger than `b`, we end up with all elements larger than the maximum of `a` and `b`.
More concisely: For any semilattice with supremum `α`, `Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)`.
|
Set.Ico_diff_left
theorem Set.Ico_diff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ico a b \ {a} = Set.Ioo a b := by
sorry
The theorem `Set.Ico_diff_left` states that for any type `α` with a defined partial order, and any two elements `a` and `b` in `α`, removing the left endpoint `a` from the left-closed right-open interval `[a, b)` (denoted by `Set.Ico a b`) results in the left-open right-open interval `(a, b)` (denoted by `Set.Ioo a b`). In other words, subtracting the singleton set `{a}` from the interval `[a, b)` yields the interval `(a, b)`. This is a theorem about the relationship between different types of intervals in an ordered set.
More concisely: For any type `α` with a partial order and any `a < b` in `α`, `Set.Ico a b \ {a} = Set.Ioo a b`.
|
Set.Ici_inter_Iic
theorem Set.Ici_inter_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ∩ Set.Iic b = Set.Icc a b := by
sorry
This theorem states that for any type `α` that has a preorder, and any two elements `a` and `b` of that type, the intersection of the set of all elements greater than or equal to `a` (`Set.Ici a`) and the set of all elements less than or equal to `b` (`Set.Iic b`) is exactly the set of all elements `x` such that `a ≤ x` and `x ≤ b` (`Set.Icc a b`). In other words, when we take the intersection of the left-closed right-infinite interval starting at `a` and the left-infinite right-closed interval ending at `b`, we get the left-closed right-closed interval from `a` to `b`.
More concisely: For any type `α` with a preorder and any `a, b ∈ α`, `Set.Icc a b = Set.Ici a ∩ Set.Iic b`.
|
Set.Icc_subset_Ico_right
theorem Set.Icc_subset_Ico_right :
∀ {α : Type u_1} [inst : Preorder α] {a b₁ b₂ : α}, b₁ < b₂ → Set.Icc a b₁ ⊆ Set.Ico a b₂
This theorem states that for any type `α` with a preorder, and for any three elements `a`, `b₁`, and `b₂` of type `α`, if `b₁` is less than `b₂`, then the left-closed right-closed interval from `a` to `b₁` is a subset of the left-closed right-open interval from `a` to `b₂`. In terms of intervals, if one interval ends at `b₁` and another ends beyond `b₁` (i.e., at `b₂`), the entire first interval is contained within the second.
More concisely: For any preorder type `α` and elements `a`, `b₁`, `b₂` with `b₁` less than `b₂`, the left-closed right-closed interval from `a` to `b₁` is a subset of the left-closed right-open interval from `a` to `b₂`.
|
Set.left_mem_Ico
theorem Set.left_mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Ico a b ↔ a < b
This theorem states that for any type `α` that has a preorder (an order that is reflexive and transitive), and for any two elements `a` and `b` of `α`, `a` is an element of the left-closed right-open interval from `a` to `b` (denoted by `Set.Ico a b` in Lean) if and only if `a` is less than `b`. This interval is defined as the set of all `x` in `α` such that `a` is less than or equal to `x` and `x` is strictly less than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` of `α`, `a` belongs to the left-closed right-open interval `[a, b)` if and only if `a` is less than `b`.
|
Set.Ioo_subset_Icc_self
theorem Set.Ioo_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Icc a b
This theorem states that for any given type `α` that has a preorder (a binary relation that is reflexive and transitive), and for any two instances `a` and `b` of this type, the left-open right-open interval (`Set.Ioo`) from `a` to `b` is a subset of the left-closed right-closed interval (`Set.Icc`) from `a` to `b`. In other words, every element that falls strictly between `a` and `b` (excluding `a` and `b` themselves) is also contained in the set of elements that includes `a` and `b` and everything in between.
More concisely: For any preorder type `α` and elements `a` and `b` of `α`, the left-open interval `Set.Ioo a b` is a subset of the left-closed right-closed interval `Set.Icc a b`.
|
Set.Ioc_subset_Icc_self
theorem Set.Ioc_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b ⊆ Set.Icc a b
The theorem `Set.Ioc_subset_Icc_self` states that for any type `α` that has a preorder (a relation that is reflexive and transitive), and for any two elements `a` and `b` of that type, the left-open right-closed interval from `a` to `b` (denoted `Set.Ioc a b`), is a subset of the left-closed right-closed interval from `a` to `b` (denoted `Set.Icc a b`). In other words, all elements `x` that satisfy `a < x ≤ b` also satisfy `a ≤ x ≤ b`.
More concisely: For any type `α` with a preorder and any `a ≤ b` in `α`, `Set.Ioc a b` (the left-open right-closed interval from `a` to `b`) is a subset of `Set.Icc a b` (the left-closed right-closed interval from `a` to `b`). In other words, `Set.Ioc a b ⊆ Set.Icc a b`.
|
Set.Ioc_subset_Ioo_right
theorem Set.Ioc_subset_Ioo_right :
∀ {α : Type u_1} [inst : Preorder α] {a b₁ b₂ : α}, b₁ < b₂ → Set.Ioc a b₁ ⊆ Set.Ioo a b₂
The theorem `Set.Ioc_subset_Ioo_right` states that for any type `α` equipped with a preorder, and for any three elements `a`, `b₁`, and `b₂` of that type, if `b₁` is less than `b₂`, then the left-open right-closed interval from `a` to `b₁` (denoted `Set.Ioc a b₁`) is a subset of the left-open right-open interval from `a` to `b₂` (denoted `Set.Ioo a b₂`). In other words, if `b₁` is strictly less than `b₂`, any element `x` that is strictly greater than `a` and less than or equal to `b₁` is also strictly less than `b₂`.
More concisely: For any type equipped with a preorder, if `a` is in the left-open right-closed interval `[a, b₁]` and `b₁` is strictly less than `b₂`, then `a` is also in the left-open right-open interval `[a, b₂]`.
|
Set.Ioi_inter_Ioi
theorem Set.Ioi_inter_Ioi :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a ∩ Set.Ioi b = Set.Ioi (a ⊔ b)
The theorem `Set.Ioi_inter_Ioi` states that for any type `α` with a linear order and any two elements `a` and `b` of `α`, the intersection of the sets of elements that are greater than `a` and greater than `b` (denoted `Set.Ioi a` and `Set.Ioi b` respectively) is equal to the set of elements that are greater than the maximum of `a` and `b` (denoted `Set.Ioi (a ⊔ b)`). In mathematical terms, this can be written as $(a, +\infty) \cap (b, +\infty) = (\max(a, b), +\infty)$.
More concisely: For any type `α` with a linear order and any `a, b ∈ α`, `Set.Ioi a ∩ Set.Ioi b = Set.Ioi (a ⊔ b)`. In other words, `(a, +∞) ∩ (b, +∞) = (max(a, b), +∞)`.
|
Set.dual_Ioc
theorem Set.dual_Ioc :
∀ {α : Type u_1} [inst : Preorder α] {a b : α},
Set.Ioc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ico b a
This theorem states that for any preorder set `α` and any two elements `a` and `b` of `α`, the left-open right-closed interval (denoted as `Set.Ioc`) between `a` and `b` under the dual order is equivalent to the preimage of the left-closed right-open interval (denoted as `Set.Ico`) between `b` and `a` under the original order. This theorem essentially expresses the dual relationship between the open-closed and closed-open intervals in a given order and its dual order.
More concisely: For any preorder set `α` and elements `a` and `b` of `α`, the left-open right-closed interval `Set.Ioc a b` under the dual order is equivalent to the preimage of the left-closed right-open interval `Set.Ico b a` under the original order.
|
Set.mem_Ioo
theorem Set.mem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioo a b ↔ a < x ∧ x < b
This theorem states that for any type α with a preorder relation, and any elements a, b, and x of α, x is an element of the left-open right-open interval between a and b (denoted `Set.Ioo a b`) if and only if a is less than x and x is less than b. It implies that membership in the interval `Set.Ioo a b` is equivalent to satisfying the two inequalities `a < x` and `x < b`.
More concisely: For any preordered type α and elements a, b, x of α, x lies in the open interval (a, b) if and only if a < x and x < b.
|
Set.Icc_bot
theorem Set.Icc_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, Set.Icc ⊥ a = Set.Iic a := by
sorry
The theorem `Set.Icc_bot` states that for any type `α` that has both an order relation (`Preorder α`) and a least element (`OrderBot α`), the interval [`⊥`, `a`] which includes all elements `x` satisfying `⊥ ≤ x ≤ a`, is equal to the interval (`-∞`, `a`] or `Set.Iic a` which includes all elements `x` satisfying `x ≤ a`. This makes sense because `⊥` is the least element in `α`, so any `x` in `α` should satisfy `⊥ ≤ x`, essentially reducing the interval [`⊥`, `a`] to (`-∞`, `a`].
More concisely: For any type `α` with a preorder and a least element, the intervals `[OrderBot α, a]` and `(-\infty, a]` are equal.
|
Set.mem_Ioc
theorem Set.mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioc a b ↔ a < x ∧ x ≤ b
This theorem states that for any type `α` with a preorder relation, and for any elements `a`, `b`, and `x` of this type, `x` belongs to the interval `Ioc a b` (which represents the set of elements greater than `a` and less than or equal to `b`) if and only if the two conditions `a < x` and `x ≤ b` are both satisfied. In other words, the theorem provides a characterization of membership in the left-open right-closed interval in terms of the preorder relation on the type `α`.
More concisely: For any type `α` with a preorder relation, an element `x` belongs to the left-open right-closed interval `Ioc a b` if and only if `a < x` and `x ≤ b`.
|
Set.Ioo_union_right
theorem Set.Ioo_union_right :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a < b → Set.Ioo a b ∪ {b} = Set.Ioc a b
This theorem states that for any type `α` that has a partial order, given two elements `a` and `b` in `α` such that `a < b`, the union of the open interval from `a` to `b` and the singleton set containing `b` equals the half-open interval from `a` to `b`. In other words, if we have a set of elements strictly between `a` and `b`, and another set containing only `b`, their union forms a set of elements that are strictly greater than `a` and less than or equal to `b`.
More concisely: For any type `α` with a partial order, the union of the open interval from `a` to `b` (elements strictly between `a` and `b`) and the singleton set `{b}` equals the half-open interval from `a` to `b` (elements strictly greater than `a` and less than or equal to `b`).
|
Set.compl_Ioi
theorem Set.compl_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, (Set.Ioi a)ᶜ = Set.Iic a
This theorem states that for any type `α` with a linear order and any element `a` of type `α`, the complement of the set of elements greater than `a` (denoted as `Set.Ioi a`) is equal to the set of elements that are less than or equal to `a` (denoted as `Set.Iic a`). In other words, in a linearly ordered set, every element not in the set of those strictly greater than a certain value is either equal to or less than that value.
More concisely: In a linearly ordered set, the complement of the set of elements strictly greater than a given element is equal to the set of elements less than or equal to that element.
|
Set.Ico_subset_Ici_self
theorem Set.Ico_subset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico a b ⊆ Set.Ici a
The theorem `Set.Ico_subset_Ici_self` states that for any type `α` with a preorder, and for all `a` and `b` of type `α`, the left-closed right-open interval from `a` to `b` is a subset of the left-closed right-infinite interval starting at `a`. In mathematical terms, this means that for all `x` such that `a ≤ x < b`, it is also true that `a ≤ x`.
More concisely: For any type `α` with a preorder and all `a < b` in `α`, the left-closed right-open interval `[a, b) is a subset of the left-closed right-infinite interval `[a, ∞)`.
|
Set.Ico_union_right
theorem Set.Ico_union_right :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Ico a b ∪ {b} = Set.Icc a b
The theorem `Set.Ico_union_right` states that for any type `α` that has a partial order, and any two elements `a` and `b` of that type where `a` is less than or equal to `b`, the union of the left-closed right-open interval from `a` to `b` and the set containing `b` alone is equal to the left-closed right-closed interval from `a` to `b`. In other words, if we have an interval from `a` to `b` that includes `a` but not `b`, and we add `b` to this set, we get the interval from `a` to `b` that includes both `a` and `b`. In mathematical terms, given $a \leq b$, then $[a, b) \cup \{b\} = [a, b]$ where $[a, b)$ and $[a, b]$ denote left-closed right-open and left-closed right-closed intervals respectively.
More concisely: For any type `α` with a partial order, and `a ≤ b`, the union of the left-closed right-open interval `[a, b)` and the singleton set `{b}` equals the left-closed right-closed interval `[a, b]`. In mathematical notation: `[a, b) ∪ {b} = [a, b]`.
|
Set.Ioo_subset_Ioi_self
theorem Set.Ioo_subset_Ioi_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Ioi a
This theorem states that for any type `α` which has a preorder (i.e., a structure where the elements can be compared for an order), and for any two elements `a` and `b` of this type, the left-open right-open interval from `a` to `b` is a subset of the left-open right-infinite interval starting from `a`. In mathematical terms, if `a` and `b` are elements of a set with a preorder, then `(a, b) ⊆ (a, ∞)`.
More concisely: For any type `α` with a preorder and any `a, b ∈ α` with `a < b`, the interval `(a, b)` is a subset of the interval `(a, ∞)`.
|
Set.Icc_union_Icc_eq_Icc
theorem Set.Icc_union_Icc_eq_Icc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Icc a b ∪ Set.Icc b c = Set.Icc a c := by
sorry
This theorem states that for any type `α` that has a linear order and any three elements `a`, `b`, and `c` of this type such that `a` is less than or equal to `b` and `b` is less than or equal to `c`, the union of the interval from `a` to `b` and the interval from `b` to `c` is equal to the interval from `a` to `c`. In mathematical terms, given $a \leq b \leq c$, we have $[a,b] \cup [b,c] = [a,c]$ where $[a,b]$ and $[b,c]$ denote the closed intervals from `a` to `b` and from `b` to `c`, respectively.
More concisely: For any type `α` with a linear order, if `a ≤ b ≤ c` then `[a, b] ∪ [b, c] = [a, c]`, where `[a, b]` and `[b, c]` denote the closed intervals from `a` to `b` and from `b` to `c`, respectively.
|
Set.Ici_subset_Ioi
theorem Set.Ici_subset_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ⊆ Set.Ioi b ↔ b < a
The theorem `Set.Ici_subset_Ioi` states that for all types `α` equipped with a preorder, and for all elements `a` and `b` of type `α`, the left-closed right-infinite interval starting from `a` is a subset of the left-open right-infinite interval starting from `b` if and only if `b` is less than `a`. In mathematical terms, this is saying that for all `a` and `b`, the set of all `x` such that `a ≤ x` is contained in the set of all `x` such that `b < x` exactly when `b < a`.
More concisely: For all preordered types `α` and elements `a` and `b` of `α`, `{x : α | a ≤ x}` is subset of `{x : α | b < x}` if and only if `b < a`.
|
Set.Icc_eq_empty
theorem Set.Icc_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a ≤ b → Set.Icc a b = ∅
This theorem states that for any type `α` that has a preorder (a reflexive and transitive binary relation) and for any two elements `a` and `b` of this type, if `a` is not less than or equal to `b`, then the set of all elements `x` such that `a ≤ x ≤ b` (denoted as `Set.Icc a b` and otherwise known as a closed interval) is empty. In other words, if the lower bound `a` is greater than the upper bound `b`, there are no elements `x` that can satisfy the conditions for being in the interval, hence the interval is empty.
More concisely: For any preorder type `α` and elements `a` and `b` of `α` with `a > b`, the interval `Set.Icc a b` is empty.
|
Set.Ioc_subset_Ioi_self
theorem Set.Ioc_subset_Ioi_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b ⊆ Set.Ioi a
This theorem states that for all types `α` equipped with a preorder, and for all elements `a` and `b` of type `α`, the left-open right-closed interval from `a` to `b` (denoted as `Set.Ioc a b`) is included in the left-open right-infinite interval starting from `a` (denoted as `Set.Ioi a`). In other words, any element `x` that is strictly greater than `a` and less than or equal to `b` is also strictly greater than `a` with no upper bound, hence the interval `(a, b]` is a subset of the interval `(a, ∞)`.
More concisely: For all types `α` with a preorder and all `a : α` and `b : α` with `a < b`, the left-open right-closed interval `Set.Ioc a b` is a subset of the left-open right-infinite interval `Set.Ioi a`.
|
Set.Ioc_subset_Iic_self
theorem Set.Ioc_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b ⊆ Set.Iic b
The theorem `Set.Ioc_subset_Iic_self` states that for any type `α` that has a preorder relation, and for any two elements `a` and `b` of this type, the left-open right-closed interval from `a` to `b` is a subset of the right-closed interval extending to negative infinity at `b`. In mathematical terms, this means that for all `x` such that `a < x ≤ b`, we also have `x ≤ b`.
More concisely: For any type `α` with a preorder relation and any `a, b ∈ α` with `a < b`, the left-open right-closed interval `[a, b)` is subset of the right-closed interval `[a, b]`.
|