Finset.exists_card_fiber_lt_of_card_lt_nsmul
theorem Finset.exists_card_fiber_lt_of_card_lt_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
[inst_1 : LinearOrderedCommSemiring M],
↑s.card < t.card • b → ∃ y ∈ t, ↑(Finset.filter (fun x => f x = y) s).card < b
The theorem `Finset.exists_card_fiber_lt_of_card_lt_nsmul` is a version of the pigeonhole principle for finite sets, specifically stated for "pigeons counted by heads". Given two finite sets `s` and `t` of types `α` and `β` respectively, a function `f` from `α` to `β`, and a value `b` of some linearly ordered commutative semiring `M`, the theorem states that if the cardinality (size) of `s` is less than the cardinality of `t` multiplied by `b`, then there exists an element `y` in `t` such that the cardinality of the set of elements in `s` which map to `y` (under function `f`) is less than `b`. In simpler terms, if we distribute elements of `s` into `t` via the mapping `f`, there must be at least one element in `t` that contains fewer than `b` elements from `s`. This follows the pigeonhole principle, which intuitively states that if you try to put more pigeons into fewer pigeonholes, at least one pigeonhole must contain more than one pigeon.
More concisely: If the cardinality of a finite set is strictly smaller than the product of the cardinalities of another finite set and a positive number, then there exists an element in the larger set that maps to fewer than that number of elements in the smaller set.
|
Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to
theorem Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
(∀ a ∈ s, f a ∈ t) → t.card * n < s.card → ∃ y ∈ t, n < (Finset.filter (fun x => f x = y) s).card
This theorem is a version of the pigeonhole principle, which states that if there are more pigeons than pigeonholes, at least one pigeonhole must contain more than one pigeon. More specifically, it asserts that there is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.
In more formal terms, given a function `f` mapping elements from a finite set `s` to another finite set `t`, and a natural number `n` such that the cardinality of `t` multiplied by `n` is less than the cardinality of `s`, there exists an element `y` in `t` such that the preimage of `y` in `s` (i.e., all the elements in `s` that `f` maps to `y`) contains more than `n` elements.
In other words, if you distribute items from `s` into the "buckets" of `t` using the function `f`, and if the average number of items per bucket (rounded up) is `n`, then there must be at least one bucket that contains more than `n` items.
More concisely: If `f` is a function from a finite set `s` to a finite set `t` with `|t| * n < |s|`, then there exists `y` in `t` such that the cardinality of `f⁻¹(y)` exceeds `n`.
|
Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul
theorem Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ a ∈ s, f a ∈ t) →
(s.sum fun x => w x) < t.card • b → ∃ y ∈ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) < b
This theorem is a version of the pigeonhole principle for a finite set, considering pigeons with weights and using strict inequality. It states that if we have a finite set of items (pigeons), each with a weight, if the total weight of all items is less than the quantity of pigeonholes times a certain weight `b`, then there must exist at least one pigeonhole where the total weight of the items in it is less than `b`. This is under the condition that the function `f` maps each item from the set `s` to a pigeonhole in the set `t`. In formal terms, given any function `f : α → β` from a finite set `s` of type `α` to a finite set `t` of type `β`, and a weight function `w : α → M` from `s` to the weights in `M`, if the total sum of the weights of `s` is less than the cardinality of `t` times `b`, there exists an element `y` in `t` such that the sum of the weights of the elements in `s` that map to `y` is less than `b`.
More concisely: Given a finite function `f : α → β` from a finite set `α` to a finite set `β`, and a weight function `w : α → M` such that the total weight `∑ x in α, w x < card β × b`, there exists a `y in β` with `∑ x in f⁻¹{y}, w x < b`.
|
Fintype.exists_sum_fiber_le_of_sum_le_nsmul
theorem Fintype.exists_sum_fiber_le_of_sum_le_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {w : α → M} {b : M} [inst_3 : LinearOrderedCancelAddCommMonoid M] [inst_4 : Nonempty β],
(Finset.univ.sum fun x => w x) ≤ Fintype.card β • b →
∃ y, ((Finset.filter (fun x => f x = y) Finset.univ).sum fun x => w x) ≤ b
This theorem, known as a version of the Pigeonhole Principle, states that given a finite set of items (pigeons) of different types (weights) and a function mapping each item to a pigeonhole, if the total weight of all items is less than or equal to the product of the number of pigeonholes and a certain weight `b`, then there exists a pigeonhole such that the total weight of items in it is less than or equal to `b`. The conditions are formalized in terms of type theorists' structures: a finite type `α` of items, a finite type `β` of pigeonholes, a weight function `w : α → M` from items to a linear ordered cancel additive commutative monoid `M`, a function `f : α → β` from items to pigeonholes, and a weight `b : M`. The theorem also assumes that the type `β` of pigeonholes is nonempty.
More concisely: Given a finite set of items with distinct weights, a function mapping each item to a pigeonhole, and a weight `b` such that the total weight of all items is less than or equal to the product of the number of pigeonholes and `b`, there exists a pigeonhole containing items with total weight less than or equal to `b`.
|
Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
theorem Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ y ∉ t, 0 ≤ (Finset.filter (fun x => f x = y) s).sum fun x => w x) →
t.Nonempty →
(s.sum fun x => w x) ≤ t.card • b → ∃ y ∈ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) ≤ b
This theorem is a generalized version of the pigeonhole principle, also known as the box principle, which involves "pigeons" with certain weights and a finite number of "pigeonholes". More specifically, the theorem states that if we have a finite set of "pigeons" each assigned a certain weight, and they are sorted into a finite number of pigeonholes, under certain conditions, there exists at least one pigeonhole such that the total weight of the pigeons in it is less than or equal to a given value `b`.
The conditions include: (1) the total weight of all the pigeons is less than or equal to `n • b`, where `n` is the number of pigeonholes, (2) for all pigeonholes that do not contain any pigeons, the total weight is nonnegative, and (3) the set of pigeonholes is not empty.
The function `f` is used to assign each "pigeon" to a "pigeonhole", and `w` is used to assign a weight to each "pigeon". The function `Finset.filter (fun x => f x = y) s` helps to identify all pigeons in a specific pigeonhole `y`. The theorem asserts that under the conditions mentioned, there exists a pigeonhole (`y ∈ t`) where the total weight of the pigeons (`(Finset.filter (fun x => f x = y) s).sum fun x => w x`) is less than or equal to `b`.
More concisely: Given a finite set of pigeons with weights and a finite number of pigeonholes, if the total weight of all pigeons is less than or equal to the product of the number of pigeonholes and a given weight limit, and there are no empty pigeonholes with negative total weight, then there exists a pigeonhole with total weight less than or equal to the weight limit.
|
Fintype.exists_le_card_fiber_of_nsmul_le_card
theorem Fintype.exists_le_card_fiber_of_nsmul_le_card :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {b : M} [inst_3 : LinearOrderedCommSemiring M] [inst_4 : Nonempty β],
Fintype.card β • b ≤ ↑(Fintype.card α) → ∃ y, b ≤ ↑(Finset.filter (fun x => f x = y) Finset.univ).card
This theorem is a statement of the strong pigeonhole principle for finite types. Given a function `f` mapping elements from a finite type `α` to another finite type `β`, and a number `b` such that the cardinality of `β` times `b` is less than or equal to the cardinality of `α`, the theorem asserts that there exists an element `y` in `β` such that the preimage of `y` under `f` contains at least `b` elements. In other words, there is at least one 'pigeonhole' (`y`) that contains `b` or more 'pigeons' (elements of `α` that map to `y` via `f`). The theorem assumes the existence of a decidable equality on `β`, the finiteness of `α` and `β`, and the non-emptiness of `β`. Moreover, `b` belongs to a type `M` that is a linearly ordered commutative semiring.
More concisely: Given a function between finite types with image size smaller than or equal to the size of the domain, there exists an image element with domain elements mapping to it in cardinality greater than or equal to the image size.
|
Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum
theorem Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ a ∈ s, f a ∈ t) →
t.Nonempty →
(t.card • b ≤ s.sum fun x => w x) → ∃ y ∈ t, b ≤ (Finset.filter (fun x => f x = y) s).sum fun x => w x
The theorem `Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum` represents a version of the pigeonhole principle, which is weighted and involves non-strict inequality. It states that if we have a finite set `s` of elements of type `α` where each element is associated with a weight function `w : α → M` and a mapping `f : α → β` to another finite set `t` of elements of type `β`, then if the total weight of the elements in `s` (calculated as the sum of the weights of each element) is greater than or equal to the product of the cardinality of `t` and a certain value `b`, and `t` is nonempty, then there exists an element `y` in `t` such that the total weight of the elements in `s` that map to `y` is greater than or equal to `b`. This essentially means that if we distribute the elements of `s` into the "pigeonholes" represented by `t`, there is at least one "pigeonhole" whose total weight (sum of the weights of the elements in that pigeonhole) is at least `b`.
More concisely: If `s` is a finite set of elements each with weight `w` and mapped to a nonempty set `t` via function `f`, and the total weight of `s` is greater than or equal to the product of `t`'s cardinality and a value `b`, then there exists an element `y` in `t` with the total weight of elements mapped to `y` being at least `b`.
|
Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul
theorem Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ a ∈ s, f a ∈ t) →
t.Nonempty →
(s.sum fun x => w x) ≤ t.card • b → ∃ y ∈ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) ≤ b
This theorem is a version of the Pigeonhole Principle. It states that if you have a finite set of "pigeons" (elements of some type `α`), each with a certain "weight" (`w`), and you sort them into a finite number of "pigeonholes" (`t`, a finite set of type `β`), according to some function `f : α → β` (such that each "pigeon" is mapped to a valid "pigeonhole"), then under certain conditions, there exists a pigeonhole such that the total weight of the pigeons in that pigeonhole is less than or equal to a given value `b`.
The conditions are as follows: (1) the total weight of all the "pigeons" is less than or equal to the number of "pigeonholes" multiplied by `b` (i.e., `(s.sum fun x => w x) ≤ t.card • b`), and (2) there is at least one "pigeonhole" (i.e., `t` is nonempty).
In this context, `Finset.filter (fun x => f x = y) s` represents the set of all "pigeons" that are sorted into the "pigeonhole" `y`, and `(Finset.filter (fun x => f x = y) s).sum fun x => w x` is the total weight of those "pigeons". So, the conclusion `∃ y ∈ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) ≤ b` means that there exists a "pigeonhole" such that the total weight of the "pigeons" in that hole is less than or equal to `b`.
More concisely: Given a finite set of elements with weights and a function mapping them to finite pigeonholes, if the total weight is less than or equal to the number of pigeonholes times a given weight limit, then there exists a pigeonhole with total weight less than or equal to the weight limit.
|
Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum
theorem Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ a ∈ s, f a ∈ t) →
(t.card • b < s.sum fun x => w x) → ∃ y ∈ t, b < (Finset.filter (fun x => f x = y) s).sum fun x => w x
This theorem, referred to as the Pigeonhole Principle for Finitely Many Pigeons Counted by Weight, states that given a finite set of objects `s` (pigeons) with a weight function `w : α → M` and a function `f : α → β` that maps each object to a finite set of categories `t` (pigeonholes), if the total weight of all objects is greater than the number of categories times some weight `b`, then there exists at least one category such that the total weight of the objects in this category is greater than `b`.
In other words, if we distribute objects into categories and the total weight of the objects exceeds the total number of categories times a certain weight, then there must be at least one category where the total weight of its objects exceeds that certain weight.
Each object `a` belongs to the set `s` and is mapped to a category `f a` which belongs to the set `t`. The condition `t.card • b < Finset.sum s fun x => w x` ensures that the total weight of the objects is greater than the product of the number of categories and the weight `b`. The conclusion `∃ y ∈ t, b < Finset.sum (Finset.filter (fun x => f x = y) s) fun x => w x` stipulates that there is at least one category `y` in `t` such that the total weight of the objects in `y` exceeds `b`.
More concisely: Given a finite set of objects with weights and a function mapping objects to finite sets (pigeonholes), if the total weight of the objects exceeds the number of categories times the weight of each category, then there exists a category with total weight greater than that weight.
|
Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul
theorem Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {w : α → M} {b : M} [inst_3 : LinearOrderedCancelAddCommMonoid M],
(Finset.univ.sum fun x => w x) < Fintype.card β • b →
∃ y, ((Finset.filter (fun x => f x = y) Finset.univ).sum fun x => w x) < b
This theorem is a statement of the pigeonhole principle for finitely many objects (pigeons) of different weights, with a strict inequality. It states that if you have two finite types, `α` and `β`, and a function `f` mapping from `α` to `β`, along with a weighted function `w` assigning weights to elements of `α`, then provided the total weight of all elements of `α` is less than the total number of elements in `β` multiplied by some value `b`, there exists an element `y` in `β` such that the sum of the weights of all elements in `α` mapped to `y` by `f` is less than `b`. Here, `α` can be thought of as the set of pigeons, `β` as the set of pigeonholes, `f` as the function assigning each pigeon to a pigeonhole, and `w` as the function determining the weight of each pigeon. The theorem then states that if the total weight of all pigeons is less than the number of pigeonholes times some value `b`, then there is a pigeonhole such that the total weight of pigeons in it is less than `b`.
More concisely: Given types `α` and `β`, a function `f` from `α` to `β`, and a weight function `w` on `α`, if the total weight of `α` is strictly less than the cardinality of `β` times some constant `b`, then there exists an element `y` in `β` such that the sum of weights of elements in `α` mapped to `y` exceeds `b` but the sum of weights of elements in `α` mapped to any other element in `β` is strictly less than `b`.
|
Fintype.exists_card_fiber_lt_of_card_lt_nsmul
theorem Fintype.exists_card_fiber_lt_of_card_lt_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {b : M} [inst_3 : LinearOrderedCommSemiring M],
↑(Fintype.card α) < Fintype.card β • b → ∃ y, ↑(Finset.filter (fun x => f x = y) Finset.univ).card < b
This theorem, named "Fintype.exists_card_fiber_lt_of_card_lt_nsmul", is a formal statement of the strong pigeonhole principle for finite types in Lean 4. It states that for any two finite types α and β and a function `f` mapping from α to β, if the size of α is less than the size of β times some number `b` (from a type `M` that forms a linear ordered commutative semiring), then there exists an element `y` in β such that the size of the preimage of `y` under `f` is less than `b`. In other words, there exists a pigeonhole (the preimage of `y`) with fewer than `b` pigeons. This is akin to saying there is at least one pigeonhole with fewer than the average number of pigeons, if we think of `b` as representing the average.
More concisely: If `f` is a function from a finite type `α` to another finite type `β` of larger size, and the size of `α` is strictly less than the size of `β` multiplied by some natural number `b`, then there exists an element `y` in `β` such that the preimage of `y` under `f` has strictly fewer than `b` elements.
|
Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum
theorem Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ y ∉ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) ≤ 0) →
t.Nonempty →
(t.card • b ≤ s.sum fun x => w x) → ∃ y ∈ t, b ≤ (Finset.filter (fun x => f x = y) s).sum fun x => w x
The theorem `Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum` states a variant of the pigeonhole principle, accounting for weight. Suppose we have a finite set of items (or "pigeons") `s` each with a certain weight `w`, and a set of categories (or "pigeonholes") `t` into which each item can be sorted based on a function `f`. If the total weight of all items is greater than or equal to `n` times a certain weight `b` (`n` being the number of categories), and the total weight of the items in each category not in `t` is nonpositive, then there exists at least one category in `t` whose total weight of items is greater than or equal to `b`. This theorem is formulated in the context of a type `M` with a linear ordered cancel-addition-commutative monoid structure, ensuring meaningful operations with weights.
More concisely: If `s` is a finite set of weights, `t` is a subset of categories, `f` is a function mapping each item in `s` to a category in `t`, `b` is a weight, and the total weight of items in each category not in `t` is nonpositive, then if the total weight of `s` is greater than or equal to `n * b` (where `n` is the number of categories in `t`), there exists a category in `t` with total weight of items greater than or equal to `b`.
|
Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to
theorem Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
[inst_1 : LinearOrderedCommSemiring M],
(∀ a ∈ s, f a ∈ t) →
t.Nonempty → t.card • b ≤ ↑s.card → ∃ y ∈ t, b ≤ ↑(Finset.filter (fun x => f x = y) s).card
The pigeonhole principle for finite sets is expressed by the theorem `Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to`. This theorem states that for any types `α`, `β` and `M` with `β` having decidable equality, and for any finite sets `s` of type `α` and `t` of type `β`, along with a function `f` from `α` to `β` and a number `b` of type `M` with a `LinearOrderedCommSemiring` instance, the following holds: If each element of `s` maps to an element of `t` and `t` is not empty, then if the cardinality of `t` multiplied by `b` is less than or equal to the cardinality of `s`, there exists an element `y` in `t` such that the preimage of `y` in `s` under the function `f` has at least `b` elements. In other words, if we assign to each element of `t` at least `b` elements of `s`, then there must be at least one element in `t` that is assigned at least `b` elements of `s`.
More concisely: Given finite sets `s` of type `α`, `t` of type `β`, a function `f` from `α` to `β`, and a number `b` in a LinearOrderedCommSemiring, if each element of `s` maps to an element of `t`, `t` is non-empty, and the product of `t`'s cardinality and `b` is less than or equal to `s`'s cardinality, then there exists an element `y` in `t` such that the preimage of `y` under `f` has size greater than or equal to `b`.
|
Fintype.exists_le_card_fiber_of_mul_le_card
theorem Fintype.exists_le_card_fiber_of_mul_le_card :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ}
[inst_3 : Nonempty β],
Fintype.card β * n ≤ Fintype.card α → ∃ y, n ≤ (Finset.filter (fun x => f x = y) Finset.univ).card
This theorem is named `Fintype.exists_le_card_fiber_of_mul_le_card` and it's a version of the strong pigeonhole principle for finite types. The theorem states that for any two finite types `α` and `β`, given a function `f` mapping from `α` to `β`, and an integer `n` such that the cardinality of `β` times `n` is less than or equal to the cardinality of `α`, there exists an element `y` in `β` such that the preimage of `y` under `f` contains at least `n` elements. The condition of the theorem requires that there is a decidable equality on `β` and that `β` is nonempty.
More concisely: Given any function from a finite type `α` to a finite type `β` with cardinality less than or equal to `n * |α|`, there exists an element `y` in `β` such that the preimage of `y` under the function contains at least `n` elements.
|
Finset.exists_card_fiber_le_of_card_le_nsmul
theorem Finset.exists_card_fiber_le_of_card_le_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
[inst_1 : LinearOrderedCommSemiring M],
t.Nonempty → ↑s.card ≤ t.card • b → ∃ y ∈ t, ↑(Finset.filter (fun x => f x = y) s).card ≤ b
The theorem `Finset.exists_card_fiber_le_of_card_le_nsmul` is a version of the pigeonhole principle for finite sets. Given a function `f`, two finite sets `s` and `t`, and a number `b` such that the cardinality of `s` is less than or equal to the cardinality of `t` multiplied by `b`, the theorem states that there exists an element `y` in `t` such that the preimage of `y` in `s` (i.e., the set of elements in `s` that `f` maps to `y`) contains no more than `b` elements. This theorem requires that the equality of elements in `t` is decidable and that `b` belongs to a linearly ordered commutative semiring.
More concisely: Given a function `f` and finite sets `s` and `t` with `|s| ≤ |t| * b` and decidable equality on `t`, there exists an element `y` in `t` such that the preimage of `y` in `s` has cardinality at most `b`.
|
Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to
theorem Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M}
[inst_1 : LinearOrderedCommSemiring M],
(∀ a ∈ s, f a ∈ t) → t.card • b < ↑s.card → ∃ y ∈ t, b < ↑(Finset.filter (fun x => f x = y) s).card
This theorem is the formulation of the Pigeonhole Principle in the context of finite sets in Lean 4. It states that for any sets `s` and `t` of types `α` and `β` respectively, and any function `f` from `α` to `β`, if all elements of `s` are mapped to `t` by `f` (`∀ a ∈ s, f a ∈ t`), and the cardinality of `t` multiplied by some number `b` from an ordered commutative semiring `M` is less than the cardinality of `s` (`t.card • b < ↑s.card`), then there exists an element `y` in `t` such that `b` is less than the cardinality of the set of elements in `s` that are mapped to `y` by `f` (`∃ y ∈ t, b < ↑(Finset.filter (fun x => f x = y) s).card`).
In simpler terms, if you assign each element in `s` to an element in `t` via function `f`, and the size of `s` is larger than `b` times the size of `t`, then there must be at least one element in `t` that has more than `b` elements from `s` mapped to it.
More concisely: If a function maps every element of a set to an element of another set, and the cardinality of the larger set is strictly greater than the cardinality of the smaller set multiplied by some positive integer, then there exists an element in the smaller set mapping to more than that integer elements in the larger set.
|
Finset.exists_card_fiber_lt_of_card_lt_mul
theorem Finset.exists_card_fiber_lt_of_card_lt_mul :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
s.card < t.card * n → ∃ y ∈ t, (Finset.filter (fun x => f x = y) s).card < n
This theorem states the pigeonhole principle for finite sets, specifically for cases where the count is determined by counting 'heads'. The principle asserts that if you have more 'pigeons' than 'pigeonholes', at least one 'pigeonhole' must contain more than one 'pigeon'. However, in this version of the principle, we are interested in the case where there is a pigeonhole with at most as many pigeons as the average number of pigeons across all pigeonholes, or in other words, "the minimum is at most the mean" when we specialize to integers.
More formally, the theorem states that for any function `f`, finite sets `s` in its domain and `t` in its codomain, and a natural number `n`, if the cardinality of `s` is less than the product of the cardinality of `t` and `n`, then there exists an element `y` in `t` such that the preimage of `y` in `s`, filtered by the condition that `f(x)` equals `y`, has less than `n` elements. This essentially means that there is at least one element in the codomain that maps to less than `n` elements in the domain, given the condition on the cardinalities of `s` and `t`.
More concisely: If the number of elements in a finite set and the product of its image size and a natural number are not equal, then there exists an image element mapping to fewer than that natural number of elements in the set.
|
Fintype.exists_card_fiber_lt_of_card_lt_mul
theorem Fintype.exists_card_fiber_lt_of_card_lt_mul :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ},
Fintype.card α < Fintype.card β * n → ∃ y, (Finset.filter (fun x => f x = y) Finset.univ).card < n
This theorem, often referred to as the "strong pigeonhole principle" for finite types, states that when you have a function `f` from one finite type `α` to another finite type `β`, and a natural number `n`, such that the cardinality of `α` is less than the cardinality of `β` multiplied by `n`, then there must exist an element `y` in `β` such that the preimage of `y` in `α` under the function `f` has less than `n` elements. This is essentially saying that if you distribute items from one set to another, there is at least one element in the second set which will receive fewer items than the average.
More concisely: If `f` is a function from a finite type `α` to a finite type `β` with `|α| < |β| * n`, then there exists `y ∈ β` such that `|f⁁⁻¹(y)| < n`.
|
Fintype.exists_card_fiber_le_of_card_le_nsmul
theorem Fintype.exists_card_fiber_le_of_card_le_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {b : M} [inst_3 : LinearOrderedCommSemiring M] [inst_4 : Nonempty β],
↑(Fintype.card α) ≤ Fintype.card β • b → ∃ y, ↑(Finset.filter (fun x => f x = y) Finset.univ).card ≤ b
This theorem, known as the strong pigeonhole principle for finite sets, states that given a function `f` from a finite type `α` to another finite type `β`, and a number `b` such that the cardinality of `α` is less than or equal to the cardinality of `β` multiplied by `b`, there must exist an element `y` in `β` such that the preimage of `y` under `f` has at most `b` elements. This is essentially saying that if we try to map more elements (the "pigeons") than the capacity of the set they are mapped into (the "pigeonholes"), multiplied by a factor `b`, then there must be at least one "pigeonhole" that contains at most `b` "pigeons". This is a generalization of the classic pigeonhole principle, and a weaker version of the theorem `Fintype.exists_card_fiber_lt_of_card_lt_nsmul`.
More concisely: Given a function between finite sets and a constant `b` such that the number of elements in the domain is less than or equal to the cardinality of the codomain multiplied by `b`, there exists an element in the codomain with at most `b` elements in its preimage.
|
Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum
theorem Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ y ∉ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) ≤ 0) →
(t.card • b < s.sum fun x => w x) → ∃ y ∈ t, b < (Finset.filter (fun x => f x = y) s).sum fun x => w x
This theorem is a variant of the pigeonhole principle, which we can refer to as the weighted pigeonhole principle. If we have a finite number of 'pigeons' in some `Finset α` where each pigeon `x` has a weight `w x` and is mapped to a 'pigeonhole' in `Finset β` via some function `f`, and each pigeonhole `y` has a weight limit `b`, the theorem states the following:
Assuming that for all pigeonholes `y` not in `t` (set of designated pigeonholes), the total weight of the pigeons in `y` is nonpositive. If the total weight of all pigeons is strictly greater than the sum of the weight limits of the pigeonholes in `t`, then there exists at least one pigeonhole in `t` such that the total weight of the pigeons in that pigeonhole is strictly greater than its weight limit `b`.
In other words, if we have more total weight than the combined weight limits of our designated pigeonholes (each weighted `b`), and we guarantee that the total weight in any non-designated pigeonhole is nonpositive, then there must exist at least one designated pigeonhole that exceeds its weight limit.
More concisely: Given a finite mapping from weights `(w : ℕ → ℝ)` and pigeons `x : Finset α` to pigeonholes `y : Finset β` with nonpositive weight in each non-designated hole `y ∉ t`, if the total weight of all pigeons exceeds the sum of weight limits of designated holes `t`, then there exists a designated hole with strictly positive overweight.
|
Nat.exists_lt_modEq_of_infinite
theorem Nat.exists_lt_modEq_of_infinite :
∀ {s : Set ℕ}, s.Infinite → ∀ {k : ℕ}, 0 < k → ∃ m ∈ s, ∃ n ∈ s, m < n ∧ k.ModEq m n
This theorem states that for any infinite set `s` of natural numbers, and any natural number `k` greater than 0, there exist two elements `m` and `n` in `s` such that `m` is less than `n` and `m` is congruent to `n` modulo `k`. In other words, if you have an infinite set of natural numbers and a non-zero natural number, you can always find two different elements in the set where the smaller one leaves the same remainder as the larger one when divided by the given natural number.
More concisely: For any infinite set of natural numbers and any positive natural number, there exist distinct elements with the same remainder when divided by that number.
|
Fintype.exists_card_fiber_le_of_card_le_mul
theorem Fintype.exists_card_fiber_le_of_card_le_mul :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ}
[inst_3 : Nonempty β],
Fintype.card α ≤ Fintype.card β * n → ∃ y, (Finset.filter (fun x => f x = y) Finset.univ).card ≤ n
The theorem `Fintype.exists_card_fiber_le_of_card_le_mul` is the strong pigeonhole principle for finite types in Lean 4. Given a function `f` mapping elements from one finite type `α` to another finite type `β`, and a natural number `n` such that the number of elements in `α` is less than or equal to the number of elements in `β` multiplied by `n`, there exists an element in `β` whose preimage under `f` contains at most `n` elements. This theorem thus states that if we distribute items from one finite set to another, and the number of items is less than or equal to the size of the second set times a number `n`, there must be some element in the second set that corresponds to at most `n` items from the first set. This is a variant of the pigeonhole principle, a basic result in combinatorics.
More concisely: Given a function between finite types with the source having fewer elements than the target multiplied by a natural number, there exists a target element mapping to no more than that number of source elements.
|
Finset.exists_card_fiber_le_of_card_le_mul
theorem Finset.exists_card_fiber_le_of_card_le_mul :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
t.Nonempty → s.card ≤ t.card * n → ∃ y ∈ t, (Finset.filter (fun x => f x = y) s).card ≤ n
This theorem is a version of the pigeonhole principle for finite sets, specifically dealing with counting "pigeons" by heads. It says that if you have a function `f`, two finite sets `s` and `t` such that `s` is a domain and `t` is a codomain of `f`, and a natural number `n`. If the cardinality (i.e., the number of elements) of `s` is less than or equal to the cardinality of `t` multiplied by `n`, then there must exist an element `y` in the set `t` for which the preimage in `s` (i.e., all elements `x` in `s` for which `f(x) = y`) has no more than `n` elements. So, loosely speaking, if you try to 'spread' elements of `s` across `t` in such a way that no more than `n` elements of `s` map to any one element of `t`, and the total number of elements in `s` isn't more than `n` times the number of elements in `t`, then you can always do it. A stronger version of the statement is also available in `Finset.exists_card_fiber_lt_of_card_lt_mul`.
More concisely: If the number of elements in a finite domain is less than or equal to the number of elements in the codomain multiplied by a natural number, then there exists an element in the codomain with fewer than that number of elements in its preimage.
|
Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to
theorem Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ},
(∀ a ∈ s, f a ∈ t) → t.Nonempty → t.card * n ≤ s.card → ∃ y ∈ t, n ≤ (Finset.filter (fun x => f x = y) s).card
This theorem is a version of the pigeonhole principle, applied to finite sets `s` and `t` with elements of type `α` and `β` respectively. Here, we have a decidable equality on `β`. The theorem states that if we have a function `f : α → β` mapping each element of `s` to an element in `t`, and a natural number `n` such that the cardinality of `t` times `n` is less than or equal to the cardinality of `s`, then there exists an element `y` in `t` such that the preimage of `y` in `s` (i.e., the set of elements in `s` that `f` maps to `y`) contains at least `n` elements. This is provided that `t` is nonempty and every element of `s` gets mapped to some element in `t` by the function `f`. The theorem essentially states that if we distribute 'pigeons' from `s` to 'holes' in `t`, then at least one 'hole' must contain `n` or more 'pigeons' if the total number of 'pigeons' is at least `n` times the number of 'holes'.
More concisely: Given a function from a finite set to a nonempty finite set with fewer elements than the cardinality of the source set multiplied by a natural number, there exists an image element with at least that natural number of preimages.
|
Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
theorem Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
{w : α → M} {b : M} [inst_1 : LinearOrderedCancelAddCommMonoid M],
(∀ y ∉ t, 0 ≤ (Finset.filter (fun x => f x = y) s).sum fun x => w x) →
(s.sum fun x => w x) < t.card • b → ∃ y ∈ t, ((Finset.filter (fun x => f x = y) s).sum fun x => w x) < b
The theorem `Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul` is the strict inequality version of the pigeonhole principle for finitely many pigeons counted by weight:
If we consider a finite set of 'pigeons' `s` of type `α`, each having a weight `w` and categorized into 'pigeonholes' of type `β` by a function `f` such that all but `n` pigeonholes (represented by a finset `t` of type `β`) contain pigeons with a total weight of nonnegative value, and the total weight of all pigeons is less than `n` times a given weight `b`.
Then the theorem guarantees that there exists a pigeonhole in `t` such that the total weight of the pigeons in this pigeonhole is less than `b`. Here, `n` is the cardinality of the set of pigeonholes.
The theorem takes into account a decidable equality on `β` and a linearly ordered cancel-additive commutative monoid on the weights. This allows us to compare and manipulate the weights in a meaningful way.
More concisely: Given a finite set of pigeons with weights and a function categorizing them into non-empty pigeonholes, if the total weight of pigeons in all but `n` holes is nonnegative and the total weight of all pigeons is less than `n` times a given weight `b`, then there exists a hole with total weight less than `b`.
|
Fintype.exists_lt_card_fiber_of_nsmul_lt_card
theorem Fintype.exists_lt_card_fiber_of_nsmul_lt_card :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {b : M} [inst_3 : LinearOrderedCommSemiring M],
Fintype.card β • b < ↑(Fintype.card α) → ∃ y, b < ↑(Finset.filter (fun x => f x = y) Finset.univ).card
This theorem is a version of the strong pigeonhole principle for finite sets. It states that for any function 'f' from a finite type 'α' to another finite type 'β', and given a positive number 'b' (of a type 'M' where 'M' is a linearly ordered commutative semiring), if the number of elements in 'β' times 'b' is less than the number of elements in 'α', then there exists an element 'y' in 'β' such that 'b' is less than the number of pre-images of 'y'. In other words, there exists a 'y' in 'β' where the number of elements in 'α' that map to 'y' (the "pigeons" in the pigeonhole principle) is greater than 'b'. This corresponds to the intuition that if there are more "pigeons" than "pigeonholes", some "pigeonhole" must contain more than the average number of "pigeons".
More concisely: Given a finite function from a finite set to another finite set and a positive element in a linearly ordered commutative semiring such that the product of the sizes of the sets and the element is smaller than the size of the domain set, there exists an image element with more than that element's worth of pre-images.
|
Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum
theorem Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {w : α → M} {b : M} [inst_3 : LinearOrderedCancelAddCommMonoid M],
(Fintype.card β • b < Finset.univ.sum fun x => w x) →
∃ y, b < (Finset.filter (fun x => f x = y) Finset.univ).sum fun x => w x
This theorem is a version of the Pigeonhole Principle, considering pigeons with different weights. In particular, it states that given finite sets `α` and `β` with a function `f` mapping elements of `α` to `β`, and a weight function `w` assigning weights to elements of `α`, if the total number of elements in `β` multiplied by a certain weight `b` is less than the total weight of all elements in `α`, then there exists an element in `β` such that the total weight of its pre-images under `f` is greater than `b`. The weights and `b` are elements of an ordered additive commutative monoid `M` with cancellation.
More concisely: Given functions `f: α → β` and weight function `w: α → M` between finite sets `α` and `β` with monoid `M`, if the total weight of `α` exceeds the product of the cardinality of `β` and weight `b` in `M`, then there exists an element `y` in `β` such that the total weight of `f^(-1)(y)` exceeds `b`.
|
Fintype.exists_le_sum_fiber_of_nsmul_le_sum
theorem Fintype.exists_le_sum_fiber_of_nsmul_le_sum :
∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β]
(f : α → β) {w : α → M} {b : M} [inst_3 : LinearOrderedCancelAddCommMonoid M] [inst_4 : Nonempty β],
(Fintype.card β • b ≤ Finset.univ.sum fun x => w x) →
∃ y, b ≤ (Finset.filter (fun x => f x = y) Finset.univ).sum fun x => w x
This theorem is a version of the pigeonhole principle for finite sets where the pigeons have different weights. Specifically, it states that for types `α`, `β`, and `M`, given a function `f` from `α` to `β`, a weight function `w` from `α` to `M`, and a value `b` of type `M`, if the total number of elements in `β` (representing pigeonholes) times `b` is less than or equal to the total weight of all elements in `α` (representing weighted pigeons), then there exists an element `y` in `β` such that the total weight of all elements in `α` that map to `y` is greater than or equal to `b`. Here, the weight is assumed to be in an ordered cancelable additive commutative monoid, and it is assumed that `β` is nonempty.
More concisely: If `f: α → β` is a function, `w: α → M` is a weight function, `M` is an ordered cancelable additive commutative monoid, `β` is nonempty, `b` is an element of `M`, and the total weight of `α` is greater than or equal to the total weight of `β` multiplied by `b`, then there exists a `y` in `β` such that the weight of elements in `α` mapping to `y` is greater than or equal to `b`.
|
Fintype.exists_lt_card_fiber_of_mul_lt_card
theorem Fintype.exists_lt_card_fiber_of_mul_lt_card :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ},
Fintype.card β * n < Fintype.card α → ∃ y, n < (Finset.filter (fun x => f x = y) Finset.univ).card
This theorem is a formal statement of the strong pigeonhole principle for finite sets. It states that if you have a function `f` mapping elements from a finite type `α` to a finite type `β`, and if the total number of elements in `β` multiplied by a number `n` is less than the number of elements in `α` (i.e., `Fintype.card β * n < Fintype.card α`), then there must exist at least one element `y` in `β` such that the number of elements in `α` that map to `y` (also known as the preimage of `y` under `f`) is greater than `n`. In other words, if you think of `α` as a set of pigeons, `β` as a set of pigeonholes, and `f` as an assignment of pigeons to pigeonholes, then there must be at least one pigeonhole that houses more than `n` pigeons.
More concisely: If `f` is a function from a finite set `α` to a finite set `β` with `Fintype.card α > Fintype.card β * n`, then there exists `y ∈ β` such that the cardinality of `f⁻¹(y)` is strictly greater than `n`.
|