Commit 2023-05-16 06:36 6c44e6ae

View on Github →

feat: port Combinatorics.Hall.Basic (#3999)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Hall/Basic.lean

added theorem Finset.all_card_le_biUnion_card_iff_exists_injective

added theorem Fintype.all_card_le_filter_rel_iff_exists_injective

added theorem Fintype.all_card_le_rel_image_card_iff_exists_injective

added def hallMatchingsFunctor

added theorem hallMatchingsOn.nonempty

added def hallMatchingsOn.restrict

added def hallMatchingsOn