Finset.Colex.singleton_le_toColex
theorem Finset.Colex.singleton_le_toColex :
∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α},
{ ofColex := {a} } ≤ { ofColex := s } ↔ ∃ x ∈ s, a ≤ x
This theorem states that for any partially ordered set (type `α` with a partial order), a singleton set `{a}` is less than or equal to another set `s` in the Colex order if and only if there exists an element `x` in `s` such that `a` is less than or equal to `x`. In other words, a singleton set is considered less than or equal to another set in the Colex order if the other set contains an element that is greater than or equal to the sole element of the singleton set.
More concisely: In the Colex order of a partially ordered set, a singleton set {a} is less than or equal to set s if and only if there exists an element x in s such that a <= x.
|
Finset.Colex.IsInitSeg.total
theorem Finset.Colex.IsInitSeg.total :
∀ {α : Type u_1} [inst : LinearOrder α] {𝒜₁ 𝒜₂ : Finset (Finset α)} {r : ℕ},
Finset.Colex.IsInitSeg 𝒜₁ r → Finset.Colex.IsInitSeg 𝒜₂ r → 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
The theorem states that initial segments are nested in some way. Specifically, for any given type `α` under a linear order, and for any two initial segments `𝒜₁` and `𝒜₂` of the finset of `α`, along with a natural number `r`, if `𝒜₁` and `𝒜₂` are both initial segments of size `r`, then either `𝒜₁` is a subset of `𝒜₂` or `𝒜₂` is a subset of `𝒜₁`. In other words, if two initial segments have the same size, they are equal.
More concisely: Given a linear order on type `α`, two initial segments `𝒜₁` and `𝒜₂` of size `r` are equal.
|
Finset.Colex.toColex_le_singleton
theorem Finset.Colex.toColex_le_singleton :
∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α},
{ ofColex := s } ≤ { ofColex := {a} } ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)
The theorem `Finset.Colex.toColex_le_singleton` states that for any type `α` with a partial order and any finite set `s` of type `α` and an element `a` of type `α`, the colexicographic order (colex) set of `s` is less than or equal to the colex set containing only `a` if and only if all elements `b` in `s` are less than or equal to `a`, and if `a` is in `s`, then `b` is equal to `a`. In other words, all elements of `s` are strictly less than `a`, except possibly `a` itself, in which case `s` would be equal to the set containing only `a`.
More concisely: For any type `α` with a partial order, a finite set `s` of type `α`, and an element `a` of type `α`, the colexicographic order of `s` is less than or equal to the colexicographic order of the singleton set `{a}` if and only if all elements in `s` are less than or equal to `a` and, if `a` is in `s`, then `s` is equal to `{a}`.
|
Finset.Colex.isInitSeg_iff_exists_initSeg
theorem Finset.Colex.isInitSeg_iff_exists_initSeg :
∀ {α : Type u_1} [inst : LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [inst_1 : Fintype α],
Finset.Colex.IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s, s.card = r ∧ 𝒜 = Finset.Colex.initSeg s
This theorem states that for any type `α` that has an instance of `LinearOrder` and `Fintype`, any finite set `𝒜` of finite sets of `α`, and any natural number `r`, a set `𝒜` is a nonempty initial segment of the colexicographic order on sets of size `r` if and only if there exists a set `s` such that the cardinality of `s` equals `r` and `𝒜` equals the initial segment of the colexicographic order on sets with `s.card` elements and ending at `s`. This means that we can characterize a nonempty initial segment of the colexicographic order in terms of the existence of an `initSeg`.
More concisely: A nonempty set of finite sets of a type `α` with instances of `LinearOrder` and `Fintype` is an initial segment of the colexicographic order on sets of size `r` if and only if there exists a set `s` of size `r` whose initial segment equals the set.
|
Finset.Colex.singleton_le_singleton
theorem Finset.Colex.singleton_le_singleton :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, { ofColex := {a} } ≤ { ofColex := {b} } ↔ a ≤ b
This theorem states that for any type `α` with an established partial order, and for any two elements `a` and `b` of this type, the Colex (Colexicographic order) of the singleton set containing `a` is less than or equal to the Colex of the singleton set containing `b` if and only if `a` is less than or equal to `b`. In essence, it extends the partial order of the elements to the Colex of their singleton sets.
More concisely: For any type `α` with a partial order and for all `a, b ∈ α`, the singleton sets `{a}` and `{b}` have the same Colex order if and only if `a` and `b` are comparable in the partial order.
|
Finset.Colex.toColex_mono
theorem Finset.Colex.toColex_mono : ∀ {α : Type u_1} [inst : PartialOrder α], Monotone Finset.Colex.toColex
This theorem states that for any type `α` with a defined partial order, the function `Finset.Colex.toColex` is monotone. In simpler terms, it means that if we have two sets `s` and `t` such that `s` is a subset of `t` (denoted by `s ⊆ t`), then `s` is less than or equal to `t` in the colexicographic order (denoted by `s ≤ t`). However, the reverse is not necessarily true, because being a subset does not form a linear order.
More concisely: For any type `α` with a defined partial order, the function `Finset.Colex.toColex` maps smaller sets (in subset relation) to elements less than or equal to larger sets in the colexicographic order.
|
Finset.geomSum_le_geomSum_iff_toColex_le_toColex
theorem Finset.geomSum_le_geomSum_iff_toColex_le_toColex :
∀ {s t : Finset ℕ} {n : ℕ},
2 ≤ n → (((s.sum fun k => n ^ k) ≤ t.sum fun k => n ^ k) ↔ { ofColex := s } ≤ { ofColex := t })
The theorem `Finset.geomSum_le_geomSum_iff_toColex_le_toColex` states that for any two finite sets of natural numbers (`s` and `t`) and a natural number `n` larger than or equal to 2, the sum of the `n`-th power of each element in `s` being less than or equal to that in `t` is equivalent to `s` being less than or equal to `t` in the colexicographic order. Colexicographic order is a method of comparing sequences, where sequences are compared from right to left, rather than the more common left-to-right comparison used in lexicographic order.
More concisely: For finite sets of natural numbers s and t, and natural number n ≥ 2, the condition that the sum of the n-th power of each element in s is less than or equal to the corresponding element in the sum of the n-th power of t holds if and only if s is less than or equal to t in colexicographic order.
|
Finset.Colex.toColex_lt_singleton
theorem Finset.Colex.toColex_lt_singleton :
∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α},
{ ofColex := s } < { ofColex := {a} } ↔ ∀ b ∈ s, b < a
This theorem states that for any given type `α` with a partial order, any `Finset` `s` of type `α`, and any element `a` of type `α`, the colexicographic order (`Colex`) of `s` is less than the colexicographic order of the `Finset` containing only `a` if and only if every element of `s` is strictly less than `a`. In other words, a set is considered to be smaller than a singleton set in colexicographic order if all of its elements are smaller than the single element of the singleton set.
More concisely: For any type `α` with a partial order, a finite set `s` of `α`, and an element `a` in `α`, the colexicographic order of `s` is strictly less than the colexicographic order of the singleton set `{a}` if and only if all elements in `s` are strictly less than `a`.
|
Finset.Colex.singleton_lt_singleton
theorem Finset.Colex.singleton_lt_singleton :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, { ofColex := {a} } < { ofColex := {b} } ↔ a < b
This theorem, `Finset.Colex.singleton_lt_singleton`, states that for any two elements `a` and `b` of a type `α` that has a partial order, the colexicographic order (Colex) of a singleton set containing `a` is less than the Colex of a singleton set containing `b` if and only if `a` is less than `b` under the base order. In other words, the Colex order is an extension of the base order when we compare singleton sets.
More concisely: For any type `α` with a partial order, the Colex order of the singleton sets `{a}` and `{b}` satisfies `{a} < {b} if and only if a < b` under the base order.
|
Finset.Colex.toColex_image_le_toColex_image
theorem Finset.Colex.toColex_image_le_toColex_image :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s t : Finset α},
StrictMono f →
({ ofColex := Finset.image f s } ≤ { ofColex := Finset.image f t } ↔ { ofColex := s } ≤ { ofColex := t })
The theorem `Finset.Colex.toColex_image_le_toColex_image` states that for all types `α` and `β` with a linear order, for any strictly monotone function `f` from `α` to `β`, and for any finite sets `s` and `t` of type `α`, the colexicographic (colex) ordering of the image of `s` under `f` is less than or equal to the colex ordering of the image of `t` under `f` if and only if the colex ordering of `s` is less than or equal to the colex ordering of `t`. In other words, strictly monotone functions preserve the colex ordering between sets.
More concisely: For all types with a linear order, if `f` is a strictly monotone function and `s` and `t` are finite sets, then the colexicographic ordering of `f(s)` is less than or equal to the colexicographic ordering of `f(t)` if and only if the same holds for `s` and `t`.
|
Finset.Colex.toColex_le_toColex_of_subset
theorem Finset.Colex.toColex_le_toColex_of_subset :
∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α}, s ⊆ t → { ofColex := s } ≤ { ofColex := t }
This theorem states that for any two finite sets `s` and `t` of a certain type `α` (where `α` is equipped with a partial order), if `s` is a subset of `t`, then `s` is less than or equal to `t` in the colex (co-lexicographic) order. However, it is important to note that the converse is not true. That is, if `s` is less than or equal to `t` in the colex order, it does not imply that `s` is a subset of `t`, since inclusion does not form a linear order.
More concisely: If `s` is a subset of `t` in a finite partial ordered set `α`, then `s` is less than or equal to `t` in the colexicographic order.
|
Mathlib.Combinatorics.Colex._auxLemma.5
theorem Mathlib.Combinatorics.Colex._auxLemma.5 :
∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α},
({ ofColex := s } ≤ { ofColex := t }) = ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
This theorem, from the `Mathlib.Combinatorics.Colex` namespace, states that for any type `α` with a partial order, and any finite sets `s` and `t` of this type, `s` is less than or equal to `t` in the colexicographic order if and only if for every element `a` in `s` that is not in `t`, there exists an element `b` in `t` that is not in `s` and `a` is less than or equal to `b`. Essentially, it provides a condition for one set to be less than or equal to another in terms of the colexicographic order, using the existence of particular elements in the sets.
More concisely: For finite sets \(s\) and \(t\) of a partially ordered type \(\alpha\), \(s \subseteq t\) in the colexicographic order if and only if for every \(a \in s \setminus t\), there exists \(b \in t \setminus s\) such that \(a \leq b\).
|
Finset.Colex.toColex_lt_toColex_of_ssubset
theorem Finset.Colex.toColex_lt_toColex_of_ssubset :
∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α}, s ⊂ t → { ofColex := s } < { ofColex := t }
This theorem states that for any type `α` with a partial order, if we have two finite sets `s` and `t` of this type such that `s` is a strict subset of `t`, then in the colex order, the colex of `s` is less than the colex of `t`. However, it's important to note that the opposite direction is not necessarily true because inclusion does not present a linear order.
More concisely: For any type with a partial order `α`, if `s` and `t` are finite subsets of `α` with `s` a strict subset of `t`, then `lex s < lex t` in the colex order.
|
Finset.Colex.toColex_sdiff_le_toColex_sdiff
theorem Finset.Colex.toColex_sdiff_le_toColex_sdiff :
∀ {α : Type u_1} [inst : PartialOrder α] {s t u : Finset α} [inst_1 : DecidableEq α],
u ⊆ s → u ⊆ t → ({ ofColex := s \ u } ≤ { ofColex := t \ u } ↔ { ofColex := s } ≤ { ofColex := t })
This theorem states that for any given type `α` with a partial ordering and decidable equality, and for any three finite sets `s`, `t`, and `u` of this type, if `u` is a subset of both `s` and `t`, then the colexicographic order of `s` and `t` is unaffected by the removal of the elements of `u` from both `s` and `t`. In other words, the colexicographic order of `s \ u` and `t \ u` is the same as the colexicographic order of `s` and `t`.
More concisely: For any finite sets `s`, `t` of a type `α` with a partial ordering and decidable equality, if `u` is a subset of both `s` and `t`, then the colexicographic order of `s \ u` and `t \ u` is equal to the colexicographic order of `s` and `t`.
|
Finset.Colex.toColex.injEq
theorem Finset.Colex.toColex.injEq :
∀ {α : Type u_3} (ofColex ofColex_1 : Finset α),
({ ofColex := ofColex } = { ofColex := ofColex_1 }) = (ofColex = ofColex_1)
This theorem states that for any type `α` and any two finite sets `ofColex` and `ofColex_1` of this type, the equality of the two single-field structures `{ ofColex := ofColex }` and `{ ofColex := ofColex_1 }` is equivalent to the equality of `ofColex` and `ofColex_1` themselves. In other words, two such structures are equal if and only if their single field `ofColex` are equal.
More concisely: For any type `α` and finite sets `ofColex` and `ofColex_1` of type `α`, the single-field structures `{ ofColex := ofColex }` and `{ ofColex := ofColex_1 }` are equal if and only if `ofColex` and `ofColex_1` are equal.
|
Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex
theorem Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex :
∀ {s t : Finset ℕ} {n : ℕ},
2 ≤ n → (((s.sum fun i => n ^ i) < t.sum fun i => n ^ i) ↔ { ofColex := s } < { ofColex := t })
This theorem states that for finite sets of natural numbers, the colexicographic order is equivalent to the order induced by the `n`-ary expansion. In particular, given two finite sets of natural numbers 's' and 't', and a natural number 'n' such that 'n' is greater than or equal to 2, the sum of 'n' to the power of each element in 's' being less than the sum of 'n' to the power of each element in 't' is equivalent to 's' being less than 't' in the colexicographic order.
More concisely: For finite sets of natural numbers s and t, and natural number n ≥ 2, the sets s and t are colexicographically ordered if and only if the sum of n raised to the power of each element in s is strictly less than the sum of n raised to the power of each element in t.
|
Finset.Colex.toColex_strictMono
theorem Finset.Colex.toColex_strictMono : ∀ {α : Type u_1} [inst : PartialOrder α], StrictMono Finset.Colex.toColex
The theorem `Finset.Colex.toColex_strictMono` states that given a partial order on a type `α`, the function `Finset.Colex.toColex` (which converts a finite set to its corresponding colexicographic order) is strictly monotone. This means that if we have two finite sets `s` and `t` such that `s` is a proper subset of `t` (represented as `s ⊂ t`), then `s` is less than `t` in the colexicographic order (represented as `s < t`). However, it's important to note that the converse does not hold – having `s < t` in the colex order does not necessarily mean `s ⊂ t`, because set inclusion does not form a linear order.
More concisely: Given a finite subset `s` of a finite set `t` in a partially ordered type, `s` strictly precedes `t` in the colexicographic order. (`s ⊂ t` implies `s < t` in the colexic order, but the converse does not hold.)
|
Finset.Colex.toColex_image_lt_toColex_image
theorem Finset.Colex.toColex_image_lt_toColex_image :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s t : Finset α},
StrictMono f →
({ ofColex := Finset.image f s } < { ofColex := Finset.image f t } ↔ { ofColex := s } < { ofColex := t })
The theorem `Finset.Colex.toColex_image_lt_toColex_image` states that for all strictly monotone functions `f` and for any two finite sets `s` and `t` of a linearly ordered type `α`, the colexicographical ordering of the image of `s` under `f` is less than the colexicographical ordering of the image of `t` under `f` if and only if the colexicographical ordering of `s` is less than the colexicographical ordering of `t`. Here, colexicographical ordering (`ofColex`) is an order relation on finite sets.
More concisely: For all strictly monotone functions `f` and finite sets `s` and `t` of a linearly ordered type `α`, `ofColex (f '' s) < ofColex (f '' t)` if and only if `s` <₂` t` (lexicographic ordering).
|
Finset.Colex.forall_lt_mono
theorem Finset.Colex.forall_lt_mono :
∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} {a : α},
{ ofColex := s } ≤ { ofColex := t } → (∀ b ∈ t, b < a) → ∀ b ∈ s, b < a
This theorem states that for any two finite sets `s` and `t` of elements of any partially ordered type `α`, and for any element `a` of type `α`, if `s` is less than or equal to `t` in the colexicographic order and all elements in `t` are less than `a`, then all elements in `s` are also less than `a`.
More concisely: If `s` is a finite subset of a partially ordered type `α` less than or equal to `t` in the colexicographic order, and all elements in `t` are strictly less than `a` in `α`, then all elements in `s` are strictly less than `a`.
|
Finset.Colex.forall_le_mono
theorem Finset.Colex.forall_le_mono :
∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} {a : α},
{ ofColex := s } ≤ { ofColex := t } → (∀ b ∈ t, b ≤ a) → ∀ b ∈ s, b ≤ a
This theorem states that for any type `α` with a partial order, and for any finite sets `s` and `t` of `α`, as well as any element `a` of `α`, if `s` is less than or equal to `t` in the co-lexicographic order, and all elements of `t` are less than or equal to `a`, then all elements of `s` are also less than or equal to `a`. In simpler terms, it asserts that if `s` is below `t` in the colex order and `t` is comprised of elements smaller than or equal to a certain value, then `s` too must be comprised of elements smaller than or equal to this value.
More concisely: If `s` is co-lexicographically smaller than `t` in a partially ordered type `α`, and all elements in `t` are less than or equal to `a`, then all elements in `s` are less than or equal to `a`.
|
Finset.Colex.toColex_sdiff_lt_toColex_sdiff
theorem Finset.Colex.toColex_sdiff_lt_toColex_sdiff :
∀ {α : Type u_1} [inst : PartialOrder α] {s t u : Finset α} [inst_1 : DecidableEq α],
u ⊆ s → u ⊆ t → ({ ofColex := s \ u } < { ofColex := t \ u } ↔ { ofColex := s } < { ofColex := t })
The theorem `Finset.Colex.toColex_sdiff_lt_toColex_sdiff` states that for any given type `α` which has a partial order and decidable equality, and for any three finite sets `s`, `t`, and `u` of type `α`, if `u` is a subset of both `s` and `t`, then the colexicographic order of `s` excluding `u` being less than the colexicographic order of `t` excluding `u` is equivalent to the colexicographic order of `s` being less than the colexicographic order of `t`. In other words, the colexicographic comparison remains the same even after removing the same elements from both sets.
More concisely: For any type `α` with decidable equality and a partial order, if `u` is a subset of both finite sets `s` and `t` in `α`, then `s` << `t` in the colexicographic order if and only if `s \ u` << `t \ u` in the colexicographic order of `α \ u`.
|