Hall

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

Statistics

Metric	Count
Definitions	0
Theorems exists_bijective_of_forall_ncard_le, exists_isMatching_of_forall_ncard_le, exists_isPerfectMatching_of_forall_ncard_le, union_eq_univ_of_forall_ncard_le	4
Total	4

SimpleGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bijective_of_forall_ncard_le 📖	mathematical	IsBipartiteWith Set.ncard Set.iUnion Set Set.instMembership neighborSet	Function.Bijective Set.Elem Adj	—	Finset.all_card_le_biUnion_card_iff_exists_injective Finset.coe_biUnion Set.iUnion_congr_Prop Set.coe_toFinset Disjoint.notMem_of_mem_right IsBipartiteWith.disjoint isBipartiteWith_neighborSet_subset Set.mem_toFinset Disjoint.notMem_of_mem_left IsBipartiteWith.symm Set.mem_union union_eq_univ_of_forall_ncard_le Function.Embedding.schroeder_bernstein_of_rel Function.Injective.of_comp Subtype.val_injective mem_neighborFinset Adj.symm
exists_isMatching_of_forall_ncard_le 📖	mathematical	IsBipartiteWith Set.ncard Set.iUnion Set Set.instMembership neighborSet	Set.instHasSubset Subgraph.verts Subgraph.IsMatching	—	Finset.all_card_le_biUnion_card_iff_exists_injective Finset.coe_image Subtype.coe_preimage_self Finset.coe_biUnion Set.iUnion_congr_Prop Set.coe_toFinset Set.iUnion_coe_set Set.iUnion_exists Finset.card_image_of_injective Subtype.val_injective Set.ncard_coe_finset Disjoint.notMem_of_mem_right IsBipartiteWith.disjoint isBipartiteWith_neighborSet_subset Set.mem_toFinset mem_neighborFinset
exists_isPerfectMatching_of_forall_ncard_le 📖	mathematical	IsBipartiteWith Set.ncard Set.iUnion Set Set.instMembership neighborSet	Subgraph.IsPerfectMatching	—	exists_bijective_of_forall_ncard_le Disjoint.notMem_of_mem_right IsBipartiteWith.disjoint Set.range_comp' Function.Surjective.range_eq Function.Bijective.surjective Subtype.coe_image_univ union_eq_univ_of_forall_ncard_le Function.Bijective.existsUnique existsUnique_eq' Subgraph.isSpanning_iff
union_eq_univ_of_forall_ncard_le 📖	mathematical	IsBipartiteWith Set.ncard Set.iUnion Set Set.instMembership neighborSet	Set.instUnion Set.univ	—	Finset.all_card_le_biUnion_card_iff_exists_injective Finset.coe_biUnion Set.iUnion_congr_Prop Set.coe_toFinset Set.eq_univ_iff_forall IsBipartiteWith.mem_of_adj mem_neighborFinset

---

← Back to Index