Finset.Ico_eq_empty
theorem Finset.Ico_eq_empty :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Finset.Ico a b = ∅ := by
sorry
This theorem, titled as an "Alias of the reverse direction of `Finset.Ico_eq_empty_iff`," states that for any type `α` which has a preorder and locally finite order, and for any elements `a` and `b` of `α`, if `a` is not less than `b`, then the finite set of elements `x` such that `a ≤ x` and `x < b` is empty. In mathematical notation, this could be expressed as: if `¬a < b`, then `{x ∈ α | a ≤ x < b} = ∅`.
More concisely: For any locally finite and preordered type `α` and elements `a, b` of `α` with `a ≠ b` and `a not< b`, the set `{x ∈ α | a ≤ x < b}` is empty.
|
Finset.uIcc_subset_uIcc
theorem Finset.uIcc_subset_uIcc :
∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
a₁ ∈ Finset.uIcc a₂ b₂ → b₁ ∈ Finset.uIcc a₂ b₂ → Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂
The theorem `Finset.uIcc_subset_uIcc` states that for any type `α` that is a lattice and has a locally finite order, and any elements `a₁`, `a₂`, `b₁`, `b₂` of `α`, if `a₁` is in the set defined by `Finset.uIcc a₂ b₂` and `b₁` is in the same set, then the set defined by `Finset.uIcc a₁ b₁` is a subset of `Finset.uIcc a₂ b₂`. In other words, if `a₁` and `b₁` both lie within the interval from `a₂` to `b₂` (inclusive), then the interval from `a₁` to `b₁` (inclusive) is entirely contained within the interval from `a₂` to `b₂`.
More concisely: For any lattice type `α` with locally finite order and elements `a₁`, `a₂`, `b₁`, `b₂` in `α`, if `a₁ ∈ Finset.uIcc a₂ b₂` and `b₁ ∈ Finset.uIcc a₂ b₂`, then `Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂`.
|
Finset.Ioc_eq_cons_Ioo
theorem Finset.Ioc_eq_cons_Ioo :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
a < b → Finset.Ioc a b = Finset.cons b (Finset.Ioo a b) ⋯
This theorem, `Finset.Ioc_eq_cons_Ioo`, states that for any partially ordered type `α` that also has a locally finite order, given two elements `a` and `b` of `α` where `a` is less than `b`, then the finite set of elements `x` such that `a < x` and `x ≤ b` (`Finset.Ioc a b`) is equal to the set formed by adjoining `b` to the finite set of elements `x` such that `a < x` and `x < b` (`Finset.Ioo a b`). In other words, this theorem is establishing a relationship between the intervals `(a, b]` and `(a, b)` in the context of finite sets, showing that you can obtain the closed interval `(a, b]` by simply adding the endpoint `b` to the open interval `(a, b)`.
More concisely: For any locally finite partially ordered type `α` and elements `a < b` in `α`, the open interval `Finset.Ioo a b` equals the half-open interval `Finset.Ioc a b`.
|
Finset.Ici_eq_cons_Ioi
theorem Finset.Ici_eq_cons_Ioi :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
Finset.Ici a = Finset.cons a (Finset.Ioi a) ⋯
The theorem `Finset.Ici_eq_cons_Ioi` states that for any type `α` equipped with a partial order and a locally finite order at the top, and for any element `a` of the type `α`, the set of elements that are greater than or equal to `a` (`Finset.Ici a`) is the same as the set obtained by adding `a` to the set of elements that are strictly greater than `a` (`Finset.Ioi a`). This is represented as `Finset.cons a (Finset.Ioi a)`, where `Finset.cons` denotes the operation of creating a new set by adding an element to an existing set.
More concisely: For any locally finite ordered type `α` and element `a` in `α`, `Finset.Ici a` equals `Finset.Ioi a` as sets.
|
Finset.Icc_eq_cons_Ico
theorem Finset.Icc_eq_cons_Ico :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
a ≤ b → Finset.Icc a b = Finset.cons b (Finset.Ico a b) ⋯
This theorem states that for any partial order that's also a locally finite order, if `a` is less than or equal to `b`, then the finite set of elements `x` such that `a ≤ x ≤ b` is equal to the union of the singleton set containing `b` and the finite set of elements `x` such that `a ≤ x < b`. In other words, the interval from `a` to `b`, inclusive, can be constructed by adding `b` to the interval from `a` to `b`, exclusive. The important aspect here is that the union operation is guaranteed to be disjoint and does not require `DecidableEq α`.
More concisely: For any locally finite partial order, the interval from `a` to `b` (inclusive) equals the union of the singleton set `{b}` and the interval from `a` to `b` (exclusive).
|
Finset.card_Iio_eq_card_Iic_sub_one
theorem Finset.card_Iio_eq_card_Iic_sub_one :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
(Finset.Iio a).card = (Finset.Iic a).card - 1
This theorem states that for any partially ordered type `α` that has a locally finite order structure from the lowest ordered element, we have the following property for any element `a` of type `α`: the cardinality (or size) of the finite set of elements `x` such that `x` is strictly less than `a` equals the cardinality of the finite set of elements `x` such that `x` is less than or equal to `a`, minus one. In other words, when we remove the element `a` from the set `Finset.Iic a`, we get the set `Finset.Iio a`.
More concisely: For any locally finite partially ordered type `α`, the number of elements strictly less than any `a` in `α` equals the number of elements less than or equal to `a` minus one.
|
antitone_iff_forall_wcovBy
theorem antitone_iff_forall_wcovBy :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), Antitone f ↔ ∀ (a b : α), a ⩿ b → f b ≤ f a
The theorem `antitone_iff_forall_wcovBy` states that for any function `f` from a locally finite preorder of type `α` to another preorder of type `β`, `f` is antitone (i.e., `f` preserves the inverse of the order relation) if and only if for all pairs `(a, b)` of elements from `α` such that `a` is way-below `b` (denoted `a ⩿ b`), the value of `f` at `b` is less than or equal to the value of `f` at `a`.
More concisely: A function between locally finite preorders is antitone if and only if it maps way-below relations to suborder relations.
|
Finset.Ioo_eq_empty
theorem Finset.Ioo_eq_empty :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Finset.Ioo a b = ∅ := by
sorry
This theorem states that for any type `α` that has a preorder and is a locally finite order, and for any two elements `a` and `b` of this type, if `a` is not less than `b` then the finite set of elements `x` such that `a < x` and `x < b` is empty. In layman's terms, if our lower bound `a` is not less than the upper bound `b`, then there are no elements between `a` and `b`.
More concisely: If `α` is a type with a preorder and is locally finite, and `a` is not less than `b` in `α`, then there are no elements `x` in `α` such that `a` is less than `x` and `x` is less than `b`.
|
Finset.card_Ioc_eq_card_Icc_sub_one
theorem Finset.card_Ioc_eq_card_Icc_sub_one :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
(Finset.Ioc a b).card = (Finset.Icc a b).card - 1
This theorem states that for any given two elements `a` and `b` of an ordered and locally finite type `α`, the number of elements in the interval `(a, b]`, represented as the finite set `Finset.Ioc a b`, is equal to the number of elements in the inclusive interval `[a, b]`, represented as `Finset.Icc a b`, minus one. In other words, the cardinality of `Finset.Ioc a b` is the cardinality of `Finset.Icc a b` subtracted by one. This makes sense intuitively as the set `Finset.Ioc a b` does not include the element `a` which is included in `Finset.Icc a b`.
More concisely: The cardinality of the open interval between two elements in an ordered and locally finite type equals the cardinality of the closed interval between those elements minus one.
|
Finset.Icc_eq_cons_Ioc
theorem Finset.Icc_eq_cons_Ioc :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
a ≤ b → Finset.Icc a b = Finset.cons a (Finset.Ioc a b) ⋯
This theorem, named `Finset.Icc_eq_cons_Ioc`, states that for any type `α` that has an instance of `PartialOrder` and `LocallyFiniteOrder`, and for any two elements `a` and `b` of this type such that `a` is less than or equal to `b`, the closed interval `[a, b]` (`Finset.Icc a b`) can be represented as the union of the set containing only `a` (`a` being the element added by `Finset.cons`) and the open-closed interval `(a, b]` (`Finset.Ioc a b`). In other words, it states that adding the lower bound `a` to the set of elements strictly greater than `a` but less than or equal to `b` results in the set of all elements in the closed interval `[a, b]`.
More concisely: For any type `α` with `PartialOrder` and `LocallyFiniteOrder`, and for all `a ≤ b` in `α`, `Finset.Icc a b = Finset.cons a (Finset.Ioc a b)`.
|
strictMono_iff_forall_covBy
theorem strictMono_iff_forall_covBy :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b
A function `f` mapping from a type `α` (which is a locally finite preorder), to a type `β` (which is a preorder), is strictly monotone (i.e., if `a < b` then `f(a) < f(b)` for all `a` and `b` in `α`) if and only if `f` is strictly monotone for all pairs `(a, b)` in `α` satisfying `a ⋖ b` (i.e., `a` is covered by `b`). In other words, one can prove that `f` is strictly monotone by only checking the pairs `(a, b)` where `a` is directly covered by `b`, without needing to consider other pairs.
More concisely: A function from a locally finite preordered type to a preorder is strictly monotone if and only if it is strictly monotone on pairs where the first element is covered by the second.
|
Finset.disjoint_Ioi_Iio
theorem Finset.disjoint_Ioi_Iio :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrderBot α] (a : α),
Disjoint (Finset.Ioi a) (Finset.Iio a)
The theorem `Finset.disjoint_Ioi_Iio` states that, for any type `α` with a preorder structure and where `α` is both a locally finite order from the top and a locally finite order from the bottom, for any element `a` of `α`, the set of elements greater than `a` (`Finset.Ioi a`) is disjoint from the set of elements less than `a` (`Finset.Iio a`). In other words, there is no element `x` in `α` that can be both strictly greater than `a` and strictly less than `a` at the same time. This embodies the intuitive notion of the ordering in a set: if a number is greater than `a`, it cannot be less than `a` and vice versa.
More concisely: For any locally finite preorder type `α` with elements `a`, the sets `Finset.Ioi a` and `Finset.Iio a` are disjoint.
|
Finset.right_not_mem_Ico
theorem Finset.right_not_mem_Ico :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∉ Finset.Ico a b
The theorem `Finset.right_not_mem_Ico` states that for any type `α` with a pre-order and a locally finite order, and any elements `a` and `b` of `α`, the element `b` is not included in the finite set of elements `x` such that `a ≤ x` and `x < b`. In mathematical terms, if we denote this set as $[a, b)$, then $b \notin [a, b)$.
More concisely: For any type `α` with a pre-order and a locally finite order, and elements `a` and `b` of `α`, the element `b` is not a member of the half-open interval `[a, b)` consisting of elements `x` such that `a ≤ x` and `x < b`.
|
Finset.Icc_subset_Icc
theorem Finset.Icc_subset_Icc :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
a₂ ≤ a₁ → b₁ ≤ b₂ → Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂
This theorem, `Finset.Icc_subset_Icc`, states that for any type `α` which is equipped with a preorder and a locally finite order, and for any 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 finite set of elements `x` such that `a₁ ≤ x` and `x ≤ b₁` is a subset of the finite set of elements `x` such that `a₂ ≤ x` and `x ≤ b₂`. In other words, if the starting and ending elements of one closed interval are respectively greater than or equal to the starting and ending elements of another closed interval, then the first interval is contained within the second.
More concisely: For any locally finite preordered type `α` and elements `a₁ ≤ a₂`, `b₁ ≤ b₂` in `α`, the interval `[a₁, b₁]` is contained in the interval `[a₂, b₂]`.
|
Finset.left_not_mem_Ioc
theorem Finset.left_not_mem_Ioc :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∉ Finset.Ioc a b
This theorem states that for any type `α` that has a preorder and is a locally finite order, and for any two elements `a` and `b` of type `α`, `a` is not a member of the finite set defined as the open-closed interval Ioc(a, b). In mathematical terms, if we have a set of elements `x` such that `a < x ≤ b`, then `a` is not included in this set.
More concisely: For any locally finite preorder type `α` and elements `a` and `b` of `α` with `a < b`, `a` is not an element of the open-closed interval `Ioc(a, b)`.
|
Finset.left_mem_uIcc
theorem Finset.left_mem_uIcc :
∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∈ Finset.uIcc a b
The theorem `Finset.left_mem_uIcc` states that for any given type `α` that forms a lattice and is locally finite ordered, and for any elements `a` and `b` of type `α`, the element `a` is always a member of the set `Finset.uIcc a b`. In other words, in the set of all elements between `a` and `b` inclusive (defined in terms of the infimum and supremum of `a` and `b`), `a` is always included.
More concisely: For any locally finite ordered type `α` and elements `a`, `b` of `α`, `a` is an element of the upward closed interval `Finset.uIcc a b`.
|
Finset.Icc_self
theorem Finset.Icc_self :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a : α), Finset.Icc a a = {a}
This theorem states that for any type `α` that has a partial order and a locally finite order, the finite set of elements `x` such that `a ≤ x` and `x ≤ a` (represented by `Finset.Icc a a`) is equal to the set that contains only the element `a` (`{a}`). Essentially, when the lower and upper bounds are the same in an interval, the resulting set only contains that single element.
More concisely: For any locally finite ordered type `α`, the interval `[a := a]` is a singleton set containing `a`.
|
Finset.not_mem_Ioi_self
theorem Finset.not_mem_Ioi_self :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] {b : α}, b ∉ Finset.Ioi b
The theorem `Finset.not_mem_Ioi_self` states that for any type `α` with a partial order and a "locally finite order top" (which means that any bounded subset of `α` is finite), and for any element `b` of type `α`, `b` is not a member of the set of elements greater than `b` (denoted as `Finset.Ioi b`). In other words, there are no elements `b` such that `b` is strictly greater than itself.
More concisely: For any type `α` with a partial order and a locally finite order top, there are no elements `b` in `α` such that `b` is a member of `Finset.Ioi b`.
|
Finset.Ioo_insert_left
theorem Finset.Ioo_insert_left :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
a < b → insert a (Finset.Ioo a b) = Finset.Ico a b
This theorem states that for any two elements `a` and `b` of a type `α` that has a partial order and locally finite order, where `a` is less than `b`, and `α` has decidable equality, inserting `a` into the open interval `{x | a < x < b}` results in the half-open interval `{x | a ≤ x < b}`. In mathematical terms, for `a, b ∈ α` with `a < b`, it asserts that adding `a` to the set of elements strictly between `a` and `b` (exclusive of `a` and `b`) produces the set of elements including `a` and strictly less than `b`.
More concisely: For any type `α` with a partial order and locally finite order, if `a < b` are elements of `α` with decidable equality, then `{x | a < x < b} = {x | a ≤ x < b}`.
|
Finset.Ico_insert_right
theorem Finset.Ico_insert_right :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
a ≤ b → insert b (Finset.Ico a b) = Finset.Icc a b
The theorem `Finset.Ico_insert_right` states that for any type `α` equipped with a partial order and a locally finite order, given any two elements `a` and `b` of this type (assuming `α` has decidable equality), if `a` is less than or equal to `b`, then by inserting `b` into the finite set of elements `x` satisfying `a ≤ x` and `x < b`, we get the finite set of elements `x` satisfying `a ≤ x ≤ b`. In other words, adding the upper bound `b` to the half-open interval `[a, b)` yields the closed interval `[a, b]`.
More concisely: For any locally finite type `α` with decidable equality and partial order, if `a ≤ b` in `α`, then `a ≤ x <= b` for all `x` in the finite set obtained by inserting `b` into the set of elements less than or equal to `a`.
|
Finset.Ico_eq_cons_Ioo
theorem Finset.Ico_eq_cons_Ioo :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
a < b → Finset.Ico a b = Finset.cons a (Finset.Ioo a b) ⋯
This theorem states that for all types `α` which have a partial order and a locally finite order, and for any two elements `a` and `b` of this type where `a` is less than `b`, the finite set of elements `x` for which `a ≤ x` and `x < b` (`Finset.Ico a b`) is equivalent to the set that contains `a` and all the elements `x` for which `a < x` and `x < b` (`Finset.cons a (Finset.Ioo a b)`). In other words, the interval `[a, b)` in the set of ordered elements can be obtained by including `a` in the open interval `(a, b)`.
More concisely: For types with a partial order and locally finite order, the interval `[a, b)` consisting of elements less than or equal to `a` and strictly less than `b` is equal to the set `{a} ∪ {x | a < x < b}`, or `Finset.cons a (Finset.Ioo a b)`.
|
Finset.left_not_mem_Ioo
theorem Finset.left_not_mem_Ioo :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∉ Finset.Ioo a b
This theorem states that for any type `α` that has a preorder and a locally finite order, and for any two elements `a` and `b` of this type, the element `a` is not a member of the finite set of elements `x` such that `a < x` and `x < b`. In other words, the left endpoint `a` is not included in the open interval `(a, b)` in a finite order.
More concisely: For any type with a preorder and locally finite order, there are no elements `a` and `b` such that `a < x` and `x < b` for some `x`. In other words, endpoints do not overlap in finite orders.
|
Set.Infinite.exists_gt
theorem Set.Infinite.exists_gt :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] {s : Set α},
s.Infinite → ∀ (a : α), ∃ b ∈ s, a < b
This theorem states that for any type `α` that has a linear order and a locally finite order at the bottom, if we have an infinite set `s` of type `α`, then for any element `a` of `α`, there exists an element `b` in the set `s` such that `a` is less than `b`. In other words, given any element, there is always a larger element in the infinite set.
More concisely: For any infinite, ordered type `α` with a locally finite order at the bottom, each element `a` in `α` has an element `b` in the set `α` strictly greater than `a`.
|
Finset.card_Ico_eq_card_Icc_sub_one
theorem Finset.card_Ico_eq_card_Icc_sub_one :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
(Finset.Ico a b).card = (Finset.Icc a b).card - 1
This theorem states that for any given type `α` with a partial order and locally finite order, for any two elements `a` and `b` of that type, the cardinality (or size) of the finset of elements `x` such that `a ≤ x` and `x < b` (denoted as `Finset.Ico a b`) is equal to the cardinality of the finset of elements `x` such that `a ≤ x` and `x ≤ b` (denoted as `Finset.Icc a b`) minus one. Essentially, this theorem is saying that the size of the set of elements within the interval `[a, b)` is one less than the size of the set of elements within the interval `[a, b]`.
More concisely: For any type `α` with a locally finite partial order, the cardinality of the interval `[a, b)` is one less than the cardinality of the interval `[a, b]`.
|
monotone_iff_forall_wcovBy
theorem monotone_iff_forall_wcovBy :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b
This theorem states that for any function `f` from a type `α` to a type `β`, where `α` is a locally finite preorder and `β` is any preorder, the function `f` is monotone if and only if for all pairs `(a, b)` of elements in `α` such that `a` is weakly covered by `b` (notated as `a ⩿ b`), the value of `f` at `a` is less than or equal to the value of `f` at `b`. This theorem bridges the concept of monotonicity with the concept of locally finite orders and weak cover relation.
More concisely: For any function between locally finite preorders, the function is monotone if and only if it maps weakly covering elements to less or equal values.
|
Finset.uIcc_subset_uIcc_union_uIcc
theorem Finset.uIcc_subset_uIcc_union_uIcc :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
Finset.uIcc a c ⊆ Finset.uIcc a b ∪ Finset.uIcc b c
This theorem is a sort of triangle inequality for sets in a linear order. It states that for any type `α` equipped with a linear order and a locally finite order, and for any three elements `a`, `b`, and `c` of type `α`, the set of elements lying between `a` and `c` (inclusive) is a subset of the union of the set of elements lying between `a` and `b` (inclusive) and the set of elements lying between `b` and `c` (inclusive). This mirrors the intuition that if you have three points on a line in order, the set of all points between the first and last one includes all the points between the first and second one, and all the points between the second and third one.
More concisely: For any type `α` with a linear order and locally finite order, the set of elements between `a` and `c` (inclusive) is subset of the union of the sets between `a` and `b` (inclusive) and between `b` and `c` (inclusive).
|
le_iff_transGen_wcovBy
theorem le_iff_transGen_wcovBy :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {x y : α},
x ≤ y ↔ Relation.TransGen (fun x x_1 => x ⩿ x_1) x y
This theorem states that in any locally finite preorder of a given type, the less than or equal to (≤) relation between any two elements is equivalent to the transitive closure of the "covered by" relation (⩿) between the same elements. In other words, for any two elements in this preorder, the first is less than or equal to the second if and only if there is a chain of "covered by" relations leading from the first to the second.
More concisely: In a locally finite preorder, the reflexive, transitive closure of the "covered by" relation (⩿) is equivalent to the less than or equal to (≤) relation.
|
monotone_iff_forall_covBy
theorem monotone_iff_forall_covBy :
∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b
This theorem states that for a function `f` mapping from a type `α` to a type `β`, where `α` has the structure of a locally finite partial order and `β` is equipped with a preorder structure, `f` is monotone if and only if it maintains the order structure when applied to any two elements `a` and `b` from `α` for which `a` is covered by `b`, i.e., there is no element `c` in `α` such that `a < c < b`. In other words, `f` is monotone if it doesn't reverse the order of `a` and `b` when `a` directly precedes `b` in the order.
More concisely: A function `f` from a locally finite partially ordered type `α` to a preordered type `β` is monotone if and only if `a ≤ b` in `α` implies `f(a) ≤ f(b)` in `β`, for all `a, b` in `α` with `a` covered by `b`.
|
Finset.card_Ioo_eq_card_Icc_sub_two
theorem Finset.card_Ioo_eq_card_Icc_sub_two :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
(Finset.Ioo a b).card = (Finset.Icc a b).card - 2
This theorem states that for any two elements `a` and `b` of a type `α`, where `α` is a partially ordered set with a locally finite order, the cardinality or size of the set of elements `x` such that `a < x < b` (denoted as `Finset.Ioo a b`) is equal to the cardinality of the set of elements `x` such that `a ≤ x ≤ b` (denoted as `Finset.Icc a b`) minus 2. In other words, the set of elements strictly between `a` and `b` is two less than the set of elements inclusive of `a` and `b`.
More concisely: For any elements `a` and `b` in a locally finite partially ordered set `α`, the cardinality of the set of elements strictly between `a` and `b` is two less than the cardinality of the set of elements inclusive of `a` and `b`.
|
Finset.Iic_eq_cons_Iio
theorem Finset.Iic_eq_cons_Iio :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] (b : α),
Finset.Iic b = Finset.cons b (Finset.Iio b) ⋯
This theorem, `Finset.Iic_eq_cons_Iio`, states that for any type `α` with a partial order and where all elements are part of a locally finite order with a smallest element, and any element `b` of this type, the finset of all elements `x` such that `x` is less than or equal to `b` (`Finset.Iic b`) is equivalent to the set constructed by taking the finset of all elements `x` such that `x` is strictly less than `b` (`Finset.Iio b`), and adding `b` to it (`Finset.cons b`). This theorem essentially says that adding `b` to the set of all elements less than `b`, forms the set of all elements less than or equal to `b`.
More concisely: For any type `α` with a partial order and a smallest element, the finset of elements less than or equal to `b` equals the finset of elements strictly less than `b` followed by `b`.
|
Finset.Ico_union_Ico_eq_Ico
theorem Finset.Ico_union_Ico_eq_Ico :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
a ≤ b → b ≤ c → Finset.Ico a b ∪ Finset.Ico b c = Finset.Ico a c
This theorem states that for any given type `α` equipped with a linear order and locally finite order, and any three elements `a`, `b`, and `c` of `α` such that `a` is less than or equal to `b` and `b` is less than or equal to `c`, the union of the finite sets from `a` to `b` (`Finset.Ico a b`) and from `b` to `c` (`Finset.Ico b c`) equals the finite set from `a` to `c` (`Finset.Ico a c`). Essentially, this theorem formalizes the intuitive notion that combining two consecutive intervals gives us the overall interval.
More concisely: For any type `α` with a linear order and locally finite order, the union of the finite intervals `[a, b]` and `[b, c]` equals the finite interval `[a, c]` when `a ≤ b ≤ c`.
|
Finset.card_Ioo_eq_card_Ico_sub_one
theorem Finset.card_Ioo_eq_card_Ico_sub_one :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
(Finset.Ioo a b).card = (Finset.Ico a b).card - 1
This theorem states that for any partially ordered, locally finite type `α` and any two elements `a` and `b` of that type, the cardinality (or size) of the set of elements `x` such that `a < x` and `x < b` (represented as `Finset.Ioo a b` in Lean 4) is equal to the cardinality of the set of elements `x` such that `a ≤ x` and `x < b` (represented as `Finset.Ico a b` in Lean 4) minus 1. In other words, the set of strictly between elements is always one element less than the set of elements inclusive of the lower bound.
More concisely: The cardinality of the set of strictly between elements in a partially ordered, locally finite type is one less than the cardinality of the set of elements with the lower bound included and the upper bound excluded.
|
Finset.Icc_eq_empty
theorem Finset.Icc_eq_empty :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a ≤ b → Finset.Icc a b = ∅ := by
sorry
This theorem states that for all types `α` that have a preorder and a locally finite order, for any two elements `a` and `b` of `α`, if `a` is not less than or equal to `b`, then the finite set of elements `x` such that `a ≤ x` and `x ≤ b` (represented by `Finset.Icc a b`) is empty. In other words, if `a` is greater than `b`, there are no elements `x` that can satisfy the conditions `a ≤ x` and `x ≤ b`, hence the set is empty.
More concisely: For all types `α` with preorder and locally finite order, if `a` is not less than or equal to `b` in `α`, then the interval `[a, b]` is empty.
|
lt_iff_transGen_covBy
theorem lt_iff_transGen_covBy :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {x y : α},
x < y ↔ Relation.TransGen (fun x x_1 => x ⋖ x_1) x y
This theorem states that in a locally finite preorder of type `α`, the less-than relation `<` between any two elements `x` and `y` is equivalent to the transitive generation of the covered by relation `⋖` from `x` to `y`. In other words, `x` is less than `y` if and only if there exists a chain of elements starting at `x` and ending at `y` such that each element in the chain is covered by the next one.
More concisely: In a locally finite preorder, element `x` is less than `y` if and only if there exists a chain `x = x\_0 ⋖ x\_1 ⋖ ... ⋖ y` from `x` to `y`.
|
antitone_iff_forall_covBy
theorem antitone_iff_forall_covBy :
∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), Antitone f ↔ ∀ (a b : α), a ⋖ b → f b ≤ f a
The theorem `antitone_iff_forall_covBy` states that for all types `α` and `β` where `α` is a partial order and also locally finite, and `β` is a Preorder, a function `f` from `α` to `β` is antitone if and only if when it is restricted to pairs `a` and `b` in `α` where `a` is covered by `b`, the function value at `b` is less than or equal to the function value at `a`. In other words, `f` is antitone if reducing `a` to `b` where `a` is covered by `b` does not increase the value of the function.
More concisely: A function from a locally finite partial order type to a preorder type is antitone if and only if it decreases in value when restricting it to covered pairs.
|
Finset.not_mem_Iio_self
theorem Finset.not_mem_Iio_self :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] {b : α}, b ∉ Finset.Iio b
This theorem states that for any type `α` that is equipped with a partial order and a locally finite order, any element `b` of type `α` is not a member of the finite set of elements that are less than `b`. In other words, given a partial order on a type and a locally finite order, no element is less than itself. This corresponds to the mathematical principle that under a partial ordering, no element is strictly less than itself.
More concisely: In a partially ordered type with a locally finite order, no element is less than itself.
|
Finset.Ico_eq_empty_of_le
theorem Finset.Ico_eq_empty_of_le :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ≤ a → Finset.Ico a b = ∅ := by
sorry
This theorem states that for any type `α` which has a preorder and is also a locally finite order, if `b` is less than or equal to `a`, then the finite set of elements `x` such that `a ≤ x` and `x < b` is an empty set. In other words, there are no elements `x` that satisfy `a ≤ x` and `x < b` when `b ≤ a` in a set with a locally finite order.
More concisely: In a locally finite order preorder type `α`, there are no elements `x` such that `a ≤ x` and `x < b` for `b ≤ a`.
|
Finset.Ioc_eq_empty
theorem Finset.Ioc_eq_empty :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Finset.Ioc a b = ∅ := by
sorry
This theorem, `Finset.Ioc_eq_empty`, states that for any type `α` which has a preorder and a locally finite order, if `a` is not less than `b`, then the finite set of elements `x` such that `a < x` and `x ≤ b` (represented by `Finset.Ioc a b`) is empty. In other words, if the lower bound `a` is not less than the upper bound `b`, then there are no elements in the interval `(a, b]`.
More concisely: For any locally finite preordered type `α`, the interval `Finset.Ioc a b` is empty whenever `a ≤ b`.
|
Finset.Ico_disjoint_Ico_consecutive
theorem Finset.Ico_disjoint_Ico_consecutive :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
Disjoint (Finset.Ico a b) (Finset.Ico b c)
The theorem `Finset.Ico_disjoint_Ico_consecutive` states that for any type `α` that is a partial order and locally finite order, and for any elements `a`, `b`, and `c` of `α`, the set of elements `x` such that `a ≤ x` and `x < b` is disjoint from the set of elements `x` such that `b ≤ x` and `x < c`. In other words, there is no element `x` that belongs to both sets, where belonging to a set is defined as `x` being greater than or equal to the lower bound and less than the upper bound of the set.
More concisely: For any locally finite partial order type `α` and elements `a < b < c` in `α`, there are no elements sharing the same position in the sets `{x | a ≤ x < b}` and `{x | b ≤ x < c}`.
|
Finset.Ico_self
theorem Finset.Ico_self :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a : α), Finset.Ico a a = ∅
The theorem `Finset.Ico_self` states that for any type `α` which has a preorder relation and a locally finite order, the interval `[a, a)` represented as a finite set (`Finset`) is an empty set. In simpler terms, it says that the set of all elements `x` such that `a ≤ x < a` is empty for any `a` in some ordered set `α`.
More concisely: For any type `α` with a preorder and locally finite order, the finite set `{x : α | a ≤ x < a}` is empty for all `a` in `α`.
|
le_iff_reflTransGen_covBy
theorem le_iff_reflTransGen_covBy :
∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {x y : α},
x ≤ y ↔ Relation.ReflTransGen (fun x x_1 => x ⋖ x_1) x y
This theorem states that, in the context of a locally finite partial order, the "less than or equal to" relation (≤) is equivalent to the reflexive transitive closure of the "covered by" relation (⋖). In other words, for any two elements `x` and `y` in an arbitrary type `α` that forms a locally finite partial order, `x` is less than or equal to `y` if and only if there is a sequence of "covered by" steps starting from `x` and leading to `y`, where a "step" can be a direct "covered by" relation or a reflexive relation (i.e., a step from an element to itself).
More concisely: In a locally finite partial order, $x ≤ y$ if and only if there exists a sequence of elements $x = x\_0, x\_1, \dots, x\_n = y$ such that for all $i < n$, either $x\_i ⋖ x\_{i+1}$ or $x\_i = x\_{i+1}$.
|
strictAnti_iff_forall_covBy
theorem strictAnti_iff_forall_covBy :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Preorder β]
(f : α → β), StrictAnti f ↔ ∀ (a b : α), a ⋖ b → f b < f a
The theorem `strictAnti_iff_forall_covBy` states that for any types `α` and `β`, given `α` is a preorder and locally finite order, and `β` is a preorder, a function `f` from `α` to `β` is strictly antitone (i.e., if `a < b` then `f(b) < f(a)`) if and only if it is strictly antitone when the function `f` is applied to any two elements `a` and `b` of `α` where `a` is covered by `b` (denoted `a ⋖ b`). This means that the strict antitone property of `f` can be determined by checking the result of `f` only on pairs of elements of `α` where one element covers the other.
More concisely: For a preorder and locally finite type `α` and a preorder type `β`, a function `f` from `α` to `β` is strictly antitone if and only if for all pairs `a ⋖ b` in `α`, `f(b) < f(a)`.
|