Basic

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

Statistics

Metric	Count
Definitions hallMatchingsFunctor, hallMatchingsOn, restrict, instFintypeElemImageCoeFinsetOfDecidableEqOfSingletonSet	4
Theorems all_card_le_biUnion_card_iff_exists_injective, all_card_le_filter_rel_iff_exists_injective, all_card_le_rel_image_card_iff_exists_injective, finite, nonempty	5
Total	9

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all_card_le_biUnion_card_iff_exists_injective 📖	mathematical	—	card biUnion Finset instMembership	—	nonempty_sections_of_finite_inverse_system isDirected_le hallMatchingsFunctor.eq_1 hallMatchingsOn.finite hallMatchingsOn.nonempty le_iff_subset card_image_of_injective card_le_card

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all_card_le_filter_rel_iff_exists_injective 📖	mathematical	—	Finset.card Finset.filter Finset Finset.instMembership Finset.decidableExistsAndFinset Finset.univ	—	Finset.ext Finset.all_card_le_biUnion_card_iff_exists_injective
all_card_le_rel_image_card_iff_exists_injective 📖	mathematical	—	Finset.card card Set.Elem SetRel.image SetLike.coe Finset Finset.instSetLike instFintypeElemImageCoeFinsetOfDecidableEqOfSingletonSet SetRel Set.instMembership	—	Set.toFinset_card Finset.ext Finset.all_card_le_biUnion_card_iff_exists_injective

(root)

Definitions

Name	Category	Theorems
hallMatchingsFunctor 📖	CompOp	—
hallMatchingsOn 📖	CompOp	2 math math: hallMatchingsOn.nonempty, hallMatchingsOn.finite
instFintypeElemImageCoeFinsetOfDecidableEqOfSingletonSet 📖	CompOp	1 math math: Fintype.all_card_le_rel_image_card_iff_exists_injective

hallMatchingsOn

Definitions

Name	Category	Theorems
restrict 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite 📖	mathematical	—	Finite Set.Elem hallMatchingsOn	—	eq_1 Finset.mem_biUnion Finite.of_injective Pi.finite Finite.of_fintype
nonempty 📖	mathematical	Finset.card Finset.biUnion	Set.Elem hallMatchingsOn	—	Finset.all_card_le_biUnion_card_iff_existsInjective' Finite.of_fintype Finset.card_image_of_injective Subtype.coe_injective Finset.image_biUnion

---

← Back to Index