Documentation Verification Report

Finite

📁 Source: Mathlib/Combinatorics/Hall/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems `all_card_le_biUnion_card_iff_existsInjective'`, `hall_cond_of_compl`, `hall_cond_of_erase`, `hall_cond_of_restrict`, `hall_hard_inductive`, `hall_hard_inductive_step_A`, `hall_hard_inductive_step_B`	7
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all_card_le_biUnion_card_iff_existsInjective'` 📖	mathematical	—	`card` `biUnion` `Finset` `instMembership`	—	`HallMarriageTheorem.hall_hard_inductive` `card_image_of_injective` `card_le_card` `mem_image` `mem_biUnion`

HallMarriageTheorem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hall_cond_of_compl` 📖	mathematical	`Finset.card` `Finset.biUnion`	`Set.Elem` `Compl.compl` `Set` `Set.instCompl` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instSDiff` `Set.instMembership`	—	`Finset.card_union_of_disjoint` `Finset.card_image_of_injective` `Subtype.coe_injective` `LE.le.trans` `Finset.card_sdiff_of_subset` `Finset.biUnion_subset_biUnion_of_subset_left` `Finset.subset_union_left` `Finset.card_le_card`
`hall_cond_of_erase` 📖	mathematical	`Finset.card` `Finset.biUnion`	`Set.Elem` `setOf` `Finset.erase` `Set` `Set.instMembership`	—	`Finset.ext` `Finset.card_image_of_injective` `Subtype.coe_injective` `Finset.image_nonempty` `instIsEmptyFalse` `Finset.mem_univ` `Finset.erase_biUnion` `Finset.card_erase_of_mem` `Finset.erase_eq_of_notMem`
`hall_cond_of_restrict` 📖	mathematical	`Finset.card` `Finset.biUnion`	`Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instMembership`	—	`Finset.card_image_of_injective` `Subtype.coe_injective` `Finset.ext`
`hall_hard_inductive` 📖	mathematical	`Finset.card` `Finset.biUnion`	`Finset` `Finset.instMembership`	—	`nonempty_fintype` `Fintype.card_eq_zero_iff` `Finite.of_fintype` `hall_hard_inductive_step_A` `Mathlib.Tactic.Push.not_forall_eq` `hall_hard_inductive_step_B`
`hall_hard_inductive_step_A` 📖	—	`Fintype.card` `Finset.card` `Finset.biUnion` `Finset` `Finset.instMembership`	—	—	`Fintype.card_pos_iff` `Finset.card_pos` `Finset.singleton_biUnion` `Set.card_ne_eq` `add_zero` `Eq.le` `hall_cond_of_erase` `instIsEmptyFalse` `Finset.mem_erase`
`hall_hard_inductive_step_B` 📖	—	`Fintype.card` `Finset.card` `Finset.biUnion` `Finset` `Finset.instMembership` `Finset.Nonempty`	—	—	`Fintype.card_coe` `Finset.card_lt_iff_ne_univ` `hall_cond_of_restrict` `Fintype.card_congr'` `Finset.card_compl_lt_iff_nonempty` `hall_cond_of_compl` `Finset.mem_sdiff` `Function.Injective.dite` `Finset.sdiff_subset`

---

← Back to Index