Finset.all_card_le_biUnion_card_iff_exists_injective
theorem Finset.all_card_le_biUnion_card_iff_exists_injective :
∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] (t : ι → Finset α),
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
The theorem `Finset.all_card_le_biUnion_card_iff_exists_injective` is a version of Hall's Marriage Theorem, framed in the context of indexed families of finite sets represented as `t : ι → Finset α`. It states that a set of distinct representatives exists if and only if every union of `k` of these sets contains at least `k` elements. Here, `s.biUnion t` denotes the union of all sets `t i` for `i ∈ s`. The theorem asserts that, for any family of sets `t` indexed by type ι, the condition that every cardinally `k` subset `s` of ι has its biUnion over `t` at least as large as `k`, is equivalent to the existence of an injective function `f` from ι to type `α`, such that for every index `x` in ι, `f x` is an element of `t x`. This theorem is a generalization of `Finset.all_card_le_biUnion_card_iff_exists_injective'`, which additionally requires that ι is a finite type.
More concisely: For any indexed family of finite sets `t : ι → Finset α`, there exists an injective function from ι to α with image in `t` if and only if every cardinality `k` subset of ι has a bi Union of size at least `k`.
|
Fintype.all_card_le_filter_rel_iff_exists_injective
theorem Fintype.all_card_le_filter_rel_iff_exists_injective :
∀ {α : Type u} {β : Type v} [inst : Fintype β] (r : α → β → Prop) [inst_1 : (a : α) → DecidablePred (r a)],
(∀ (A : Finset α), A.card ≤ (Finset.filter (fun b => ∃ a ∈ A, r a b) Finset.univ).card) ↔
∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
This theorem is a version of Hall's Marriage Theorem, stated in the context of a relationship to a finite type. It asserts that there exists a transversal of the relation, i.e., an injective function from type `α` to type `β` whose graph is a subrelation of the given relation, if and only if for every subset `A` of elements of type `α`, the cardinality of `A` is less than or equal to the cardinality of the elements in the universal set of type `β` that are related to at least one element in `A`. Here, the relationship is represented by the predicate `r : α → β → Prop`. The theorem thus establishes a necessary and sufficient condition for the existence of an injective function satisfying the given relation.
More concisely: A relation between types `α` and `β` has a transversal if and only if for every subset `A` of `α`, the number of related elements in `β` to elements in `A` is greater than or equal to the size of `A`.
|
hallMatchingsOn.nonempty
theorem hallMatchingsOn.nonempty :
∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] (t : ι → Finset α),
(∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∀ (ι' : Finset ι), Nonempty ↑(hallMatchingsOn t ι')
The theorem `hallMatchingsOn.nonempty` states that for all types `ι` and `α` where `α` has a decidable equality, given a function `t` from `ι` to finite sets of `α`, if every finite subset `s` of `ι` satisfies the Hall condition - that is, the cardinality of `s` is less than or equal to the cardinality of the union of finite sets `t` over `s` - then for every finite subset `ι'` of `ι`, the set of matchings (which are injective functions from members of `ι'` to `α` such that each output belongs to the finite set `t` of its corresponding input) on `ι'` is nonempty. This theorem is part of the argument involving the lemma `Finset.all_card_le_biUnion_card_iff_existsInjective'`, which is related to Hall's Marriage Theorem in combinatorics.
More concisely: Given a function from a type with decidable equality to finite sets of another type, if every finite subset satisfies the Hall condition, then the set of injective functions from any finite subset to the values of the function is nonempty.
|
Fintype.all_card_le_rel_image_card_iff_exists_injective
theorem Fintype.all_card_le_rel_image_card_iff_exists_injective :
∀ {α : Type u} {β : Type v} [inst : DecidableEq β] (r : α → β → Prop)
[inst_1 : (a : α) → Fintype ↑(Rel.image r {a})],
(∀ (A : Finset α), A.card ≤ Fintype.card ↑(Rel.image r ↑A)) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), r x (f x)
This theorem is a variant of Hall's Marriage Theorem stated in the context of a relation between two types, `α` and `β`. The type `α` is assumed to be finite, and the image of each term of type `α` under the given relation is required to be finite (although this requirement can be relaxed if `β` is finite). The theorem states that there exists a transversal of the relation, i.e., an injective function from `α` to `β` whose graph is a subset of the original relation, if and only if for every subset of `α` consisting of `k` terms, there are at least `k` terms in `β` related to it. Here, `r : α → β → Prop` is the given relation, `Fintype.card ↑(Rel.image r ↑A)` gives the cardinality of the image of subset `A` of `α` under relation `r`, and `A.card` is the number of elements in subset `A`. The injective function `f` from `α` to `β` satisfies the property that for all `x` in `α`, `x` is related to `f(x)` by `r`.
More concisely: The Hall's Marriage Theorem states that given a finite type `α` and a relation `r : α → β → Prop` between `α` and `β` such that the image of each term of type `α` under `r` is finite, there exists an injective function from `α` to `β` whose graph is a subset of `r` if and only if for every subset `A` of `α` with `k` elements, there are at least `k` elements in `β` related to every `k` elements of `A`.
|