Finset.all_card_le_biUnion_card_iff_existsInjective'
theorem Finset.all_card_le_biUnion_card_iff_existsInjective' :
∀ {ι : Type u_1} {α : Type u_2} [inst : Finite ι] [inst : DecidableEq α] (t : ι → Finset α),
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
This theorem is a version of Hall's Marriage Theorem, described in the context of indexed families of finite sets `t : ι → Finset α`, where `ι` is a finite type. The theorem asserts that there exists a set of distinct representatives if and only if every union of `k` of the sets has at least `k` elements. This is equivalent to saying that for every subset `s` of `ι`, the cardinality of `s` is less than or equal to the cardinality of the union of the sets `t i` for each `i` in `s`. In more formal terms, this condition is represented by the statement `∀ (s : Finset ι), s.card ≤ (s.biUnion t).card`. The theorem further states that this condition holds if and only if there exists a function `f` from `ι` to `α` that is injective (meaning no two different elements in `ι` get mapped to the same element in `α`) and for each `x` in `ι`, `f(x)` belongs to the set `t(x)`. This is formally represented by the statement `∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x`.
More concisely: The Hall's Marriage Theorem states that an indexed family of finite sets `t : ι → Finset α` has a set of distinct representatives if and only if every subset of indices has a cardinality less than or equal to the cardinality of the union of the corresponding sets, and there exists an injective function mapping each index to an element in the corresponding set.
|
HallMarriageTheorem.hall_hard_inductive_step_B
theorem HallMarriageTheorem.hall_hard_inductive_step_B :
∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Fintype ι] {n : ℕ},
Fintype.card ι = n + 1 →
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) →
(∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
Fintype.card ι' ≤ n →
(∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) →
∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x) →
∀ (s : Finset ι),
s.Nonempty →
s ≠ Finset.univ → s.card = (s.biUnion t).card → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
This theorem represents the second case of the inductive step in Hall's Marriage Theorem. It states that given a type `ι` of cardinality `n + 1` and a function `t` mapping elements of `ι` to finite sets of a type `α` (with decidable equality), if for every finite set `s` of type `ι`, the cardinality of `s` is less than or equal to the cardinality of the union of the sets to which the elements of `s` map under `t`, and if the statement of Hall's Marriage Theorem holds true for all types `ι'` with cardinality less than or equal to `n`, then for every non-empty set `s` of type `ι`, if `s` is not the universal set and if the cardinality of `s` equals the cardinality of the union of the sets to which the elements of `s` map under `t`, then there exists an injective function `f` from `ι` to `α` such that every element of `ι` under `f` maps to an element in the corresponding set under `t`. In other words, it guarantees the existence of a perfect matching under the given conditions.
More concisely: Given a function mapping elements of an `(n+1)-`element set to finite sets with decidable equality such that the union of the sets to which elements map covers their domain for all subsets of smaller cardinality `n`, Hall's Marriage Theorem holds and there exists an injective function from the set to the sets' elements ensuring a perfect matching for any non-universal subset of equal cardinality.
|
HallMarriageTheorem.hall_hard_inductive
theorem HallMarriageTheorem.hall_hard_inductive :
∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Finite ι],
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
The theorem `HallMarriageTheorem.hall_hard_inductive` is a strong induction proof for the more challenging direction of Hall's Marriage Theorem. It asserts that for any types `ι` and `α`, where `α` has decidable equality, and given a function `t` from `ι` to a finite set of `α`, if for every finite subset `s` of `ι`, the cardinality of `s` is less than or equal to the cardinality of the union over `t` on `s`, then there exists an injective function `f` from `ι` to `α` such that for every element `x` in `ι`, `f(x)` belongs to `t(x)`. In other words, it establishes that under the stated conditions, it is possible to assign distinct elements of `α` to each element of `ι` in a way that respects the assignment defined by `t`.
More concisely: If for any function from a finite set to a finite set with decidable equality, every finite subset has cardinality less than or equal to the union's cardinality, then there exists an injective function mapping every element to a distinct element in its assigned set.
|
HallMarriageTheorem.hall_hard_inductive_step_A
theorem HallMarriageTheorem.hall_hard_inductive_step_A :
∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] {t : ι → Finset α} [inst_1 : Fintype ι] {n : ℕ},
Fintype.card ι = n + 1 →
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) →
(∀ {ι' : Type u} [inst_2 : Fintype ι'] (t' : ι' → Finset α),
Fintype.card ι' ≤ n →
(∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) →
∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x) →
(∀ (s : Finset ι), s.Nonempty → s ≠ Finset.univ → s.card < (s.biUnion t).card) →
∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
The theorem `HallMarriageTheorem.hall_hard_inductive_step_A` asserts that for a setup involving two types `ι` and `α` with decidable equality on `α`, and a function `t` mapping elements of `ι` to finite subsets of `α`, if the cardinality of `ι` is `n + 1`, then Hall's Marriage Theorem is true for `ι`. This is under the assumptions that (1) for any subset `s` of `ι`, the cardinality of `s` is less than or equal to the cardinality of the union of `t`-images of elements in `s`, (2) the theorem is true for any other type `ι'` of cardinality less than or equal to `n` with a similar mapping `t'`, and (3) for any non-empty proper subset `s` of `ι`, the cardinality of `s` is strictly less than the cardinality of the union of `t`-images of elements in `s`. The conclusion is the existence of an injective function `f` from `ι` to `α` such that for each element `x` of `ι`, `f(x)` is an element of the `t`-image of `x`.
In more simple terms, this theorem states a part of an inductive step used in the proof of Hall's Marriage Theorem, which is a classical result in combinatorics. It says that if the conditions of the theorem hold for smaller situations (cardinality `n` or less), and certain additional conditions hold for the current situation (cardinality `n + 1`), then the theorem is true for the current situation.
More concisely: Given types `ι` and `α` with decidable equality on `α`, a function `t` mapping elements of `ι` to finite subsets of `α`, and assuming Hall's Marriage Theorem holds for types of cardinality less than `ι` with similar mappings, if the cardinality of `ι` is `n + 1` and the union of `t`-images of any non-empty proper subset of `ι` strictly contains the subset itself, then Hall's Marriage Theorem holds for `ι` and `t`.
|