Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-12 02:51 72141fdc

View on Github →

feat(combinatorics/hall): Hall's marriage theorem (#5695) We state and prove Hall's marriage theorem with respect to fintypes and relations. Coauthor: @b-mehta @kmill

Estimated changes

Modified docs/references.bib

Created src/combinatorics/hall.lean

added theorem finset.all_card_le_bUnion_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 theorem hall_marriage_theorem.hall_cond_of_compl

added theorem hall_marriage_theorem.hall_cond_of_erase

added theorem hall_marriage_theorem.hall_cond_of_restrict

added theorem hall_marriage_theorem.hall_hard_inductive

added theorem hall_marriage_theorem.hall_hard_inductive_step

added theorem hall_marriage_theorem.hall_hard_inductive_step_A

added theorem hall_marriage_theorem.hall_hard_inductive_step_B

added theorem hall_marriage_theorem.hall_hard_inductive_zero

Modified src/data/set/finite.lean

added theorem set.card_ne_eq

added theorem set.to_finset_ne_eq_erase