Bipartite

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

Statistics

Metric	Count
Definitions `completeBipartiteGraph`, `IsBipartite`, `IsBipartiteWith`, `between`, `bipartiteDoubleCover`, `instDecidableRelAdjBetweenOfDecidablePredMemSet`, `instDecidableRelSumAdjBipartiteDoubleCover`	7
Theorems `exists_isBipartiteWith`, `subgraph`, `disjoint`, `isBipartite`, `mem_of_adj`, `mem_of_mem_adj`, `mem_of_mem_adj'`, `subgraph`, `between_adj`, `between_comm`, `between_isBipartite`, `between_isBipartiteWith`, `between_le`, `bipartiteDoubleCover_le`, `card_edgeFinset_bipartiteDoubleCover`, `completeBipartiteGraph_isContained_bipartiteDoubleCover`, `completeBipartiteGraph_isContained_iff`, `degree_le_between_add`, `degree_le_between_add_compl`, `isBipartiteWith_bipartiteAbove`, `isBipartiteWith_bipartiteBelow`, `isBipartiteWith_bipartiteDoubleCover`, `isBipartiteWith_comm`, `isBipartiteWith_degree_le`, `isBipartiteWith_degree_le'`, `isBipartiteWith_neighborFinset`, `isBipartiteWith_neighborFinset'`, `isBipartiteWith_neighborFinset_disjoint`, `isBipartiteWith_neighborFinset_disjoint'`, `isBipartiteWith_neighborFinset_subset`, `isBipartiteWith_neighborFinset_subset'`, `isBipartiteWith_neighborSet`, `isBipartiteWith_neighborSet'`, `isBipartiteWith_neighborSet_disjoint`, `isBipartiteWith_neighborSet_disjoint'`, `isBipartiteWith_neighborSet_subset`, `isBipartiteWith_neighborSet_subset'`, `isBipartiteWith_sum_degrees_eq`, `isBipartiteWith_sum_degrees_eq_card_edges`, `isBipartiteWith_sum_degrees_eq_card_edges'`, `isBipartiteWith_sum_degrees_eq_twice_card_edges`, `isBipartiteWith_support_subset`, `isBipartite_bipartiteDoubleCover`, `isBipartite_iff_exists_isBipartiteWith`, `neighborFinset_subset_between_union`, `neighborFinset_subset_between_union_compl`, `neighborSet_subset_between_union`, `neighborSet_subset_between_union_compl`	48
Total	55

SimpleGraph

Definitions

Name	Category	Theorems
`IsBipartite` 📖	MathDef	9 math math: `isBipartite_bipartiteDoubleCover`, `IsTree.isBipartite`, `IsBipartite.subgraph`, `chromaticNumber_eq_two_iff`, `chromaticNumber_le_two_iff_isBipartite`, `IsBipartiteWith.isBipartite`, `between_isBipartite`, `IsAcyclic.isBipartite`, `isBipartite_iff_exists_isBipartiteWith`
`IsBipartiteWith` 📖	CompData	7 math math: `IsBipartiteWith.subgraph`, `between_isBipartiteWith`, `IsBipartiteWith.symm`, `isBipartiteWith_bipartiteDoubleCover`, `IsBipartite.exists_isBipartiteWith`, `isBipartiteWith_comm`, `isBipartite_iff_exists_isBipartiteWith`
`between` 📖	CompOp	11 math math: `neighborSet_subset_between_union`, `between_le`, `neighborFinset_subset_between_union`, `neighborFinset_subset_between_union_compl`, `neighborSet_subset_between_union_compl`, `between_isBipartite`, `degree_le_between_add`, `between_isBipartiteWith`, `between_adj`, `between_comm`, `degree_le_between_add_compl`
`bipartiteDoubleCover` 📖	CompOp	5 math math: `bipartiteDoubleCover_le`, `isBipartite_bipartiteDoubleCover`, `completeBipartiteGraph_isContained_bipartiteDoubleCover`, `card_edgeFinset_bipartiteDoubleCover`, `isBipartiteWith_bipartiteDoubleCover`
`instDecidableRelAdjBetweenOfDecidablePredMemSet` 📖	CompOp	4 math math: `neighborFinset_subset_between_union`, `neighborFinset_subset_between_union_compl`, `degree_le_between_add`, `degree_le_between_add_compl`
`instDecidableRelSumAdjBipartiteDoubleCover` 📖	CompOp	1 math math: `card_edgeFinset_bipartiteDoubleCover`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`between_adj` 📖	mathematical	—	`Adj` `between` `Set` `Set.instMembership`	—	—
`between_comm` 📖	mathematical	—	`between`	—	—
`between_isBipartite` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`IsBipartite` `between`	—	`IsBipartiteWith.isBipartite` `between_isBipartiteWith`
`between_isBipartiteWith` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`IsBipartiteWith` `between`	—	—
`between_le` 📖	mathematical	—	`SimpleGraph` `instLE` `between`	—	—
`bipartiteDoubleCover_le` 📖	mathematical	—	`SimpleGraph` `instLE` `bipartiteDoubleCover` `completeBipartiteGraph`	—	—
`card_edgeFinset_bipartiteDoubleCover` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `bipartiteDoubleCover` `fintypeEdgeSet` `Sym2.instFintype` `instFintypeSum` `instDecidableRelSumAdjBipartiteDoubleCover`	—	`two_mul_card_edgeFinset` `Finset.card_bij` `Sym2.ind` `mem_edgeSet` `mem_edgeFinset` `Adj.symm`
`completeBipartiteGraph_isContained_bipartiteDoubleCover` 📖	mathematical	—	`IsContained` `completeBipartiteGraph` `bipartiteDoubleCover`	—	`Finset.card_pos` `LT.lt.trans_le` `Fintype.card_pos` `Eq.ge` `Finset.card_bij` `Finset.mem_toLeft` `Finset.mem_coe` `Finset.mem_toRight` `Finset.card_map`
`completeBipartiteGraph_isContained_iff` 📖	mathematical	—	`IsContained` `completeBipartiteGraph` `Finset` `Finset.card` `Fintype.card` `IsCompleteBetween` `SetLike.coe` `Finset.instSetLike`	—	`Copy.injective` `Sum.inl_injective` `Sum.inr_injective` `Finset.card_map` `Finset.mem_map` `Finset.mem_coe` `Hom.map_adj`
`degree_le_between_add` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`degree` `neighborSetFintype` `between` `SetLike.coe` `Finset` `Finset.instSetLike` `Compl.compl` `Set` `Set.instCompl` `instDecidableRelAdjBetweenOfDecidablePredMemSet` `Finset.decidableMem'` `Set.decidableCompl` `Finset.card`	—	`Finset.coe_compl` `between_isBipartiteWith` `disjoint_compl_right` `Finset.card_union_of_disjoint` `isBipartiteWith_neighborFinset_disjoint` `Finset.card_le_card` `neighborFinset_subset_between_union`
`degree_le_between_add_compl` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	`degree` `neighborSetFintype` `between` `SetLike.coe` `Finset` `Finset.instSetLike` `Compl.compl` `Set` `Set.instCompl` `instDecidableRelAdjBetweenOfDecidablePredMemSet` `Finset.decidableMem'` `Set.decidableCompl` `Finset.card` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	—	`Finset.coe_compl` `between_isBipartiteWith` `disjoint_compl_right` `Finset.card_union_of_disjoint` `isBipartiteWith_neighborFinset_disjoint'` `Finset.card_le_card` `neighborFinset_subset_between_union_compl`
`isBipartiteWith_bipartiteAbove` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`neighborFinset` `Finset.bipartiteAbove` `Adj`	—	`isBipartiteWith_neighborFinset` `Finset.bipartiteAbove.eq_1`
`isBipartiteWith_bipartiteBelow` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`neighborFinset` `Finset.bipartiteBelow` `Adj`	—	`isBipartiteWith_neighborFinset'` `Finset.bipartiteBelow.eq_1`
`isBipartiteWith_bipartiteDoubleCover` 📖	mathematical	—	`IsBipartiteWith` `bipartiteDoubleCover` `setOf`	—	`instIsEmptyFalse`
`isBipartiteWith_comm` 📖	mathematical	—	`IsBipartiteWith`	—	`IsBipartiteWith.symm`
`isBipartiteWith_degree_le` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`degree` `Finset.card`	—	`card_neighborFinset_eq_degree` `Finset.card_le_card` `isBipartiteWith_neighborFinset_subset`
`isBipartiteWith_degree_le'` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`degree` `Finset.card`	—	`card_neighborFinset_eq_degree` `Finset.card_le_card` `isBipartiteWith_neighborFinset_subset'`
`isBipartiteWith_neighborFinset` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`neighborFinset` `Finset.filter` `Adj`	—	`Finset.ext` `mem_neighborFinset` `Finset.mem_filter` `IsBipartiteWith.mem_of_mem_adj`
`isBipartiteWith_neighborFinset'` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`neighborFinset` `Finset.filter` `Adj`	—	`Finset.ext` `mem_neighborFinset` `adj_comm` `Finset.mem_filter` `IsBipartiteWith.mem_of_mem_adj'`
`isBipartiteWith_neighborFinset_disjoint` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `neighborFinset`	—	`neighborFinset_def` `Finset.disjoint_coe` `Set.coe_toFinset` `isBipartiteWith_neighborSet_disjoint`
`isBipartiteWith_neighborFinset_disjoint'` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `neighborFinset`	—	`neighborFinset_def` `Finset.disjoint_coe` `Set.coe_toFinset` `isBipartiteWith_neighborSet_disjoint'`
`isBipartiteWith_neighborFinset_subset` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`Finset` `Finset.instHasSubset` `neighborFinset`	—	`isBipartiteWith_neighborFinset` `Finset.filter_subset`
`isBipartiteWith_neighborFinset_subset'` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike` `SetLike.instMembership`	`Finset` `Finset.instHasSubset` `neighborFinset`	—	`isBipartiteWith_neighborFinset'` `Finset.filter_subset`
`isBipartiteWith_neighborSet` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`neighborSet` `setOf` `Set` `Set.instMembership` `Adj`	—	`Set.ext` `mem_neighborSet` `Set.mem_setOf_eq` `IsBipartiteWith.mem_of_mem_adj`
`isBipartiteWith_neighborSet'` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`neighborSet` `setOf` `Set` `Set.instMembership` `Adj`	—	`Set.ext` `mem_neighborSet` `adj_comm` `Set.mem_setOf_eq` `IsBipartiteWith.mem_of_mem_adj'`
`isBipartiteWith_neighborSet_disjoint` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `neighborSet`	—	`Set.disjoint_of_subset_left` `isBipartiteWith_neighborSet_subset` `Disjoint.symm` `IsBipartiteWith.disjoint`
`isBipartiteWith_neighborSet_disjoint'` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `neighborSet`	—	`Set.disjoint_of_subset_left` `isBipartiteWith_neighborSet_subset'` `IsBipartiteWith.disjoint`
`isBipartiteWith_neighborSet_subset` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`Set` `Set.instHasSubset` `neighborSet`	—	`isBipartiteWith_neighborSet` `Set.sep_subset`
`isBipartiteWith_neighborSet_subset'` 📖	mathematical	`IsBipartiteWith` `Set` `Set.instMembership`	`Set` `Set.instHasSubset` `neighborSet`	—	`isBipartiteWith_neighborSet'` `Set.sep_subset`
`isBipartiteWith_sum_degrees_eq` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.sum` `Nat.instAddCommMonoid` `degree`	—	`Finset.sum_attach` `Finset.sum_congr` `isBipartiteWith_bipartiteAbove` `Subtype.prop` `isBipartiteWith_bipartiteBelow` `Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`
`isBipartiteWith_sum_degrees_eq_card_edges` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.sum` `Nat.instAddCommMonoid` `degree` `neighborSetFintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `isBipartiteWith_sum_degrees_eq_twice_card_edges` `Finset.sum_union` `Finset.disjoint_coe` `IsBipartiteWith.disjoint` `two_mul` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `isBipartiteWith_sum_degrees_eq`
`isBipartiteWith_sum_degrees_eq_card_edges'` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.sum` `Nat.instAddCommMonoid` `degree` `neighborSetFintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`isBipartiteWith_sum_degrees_eq_card_edges` `IsBipartiteWith.symm`
`isBipartiteWith_sum_degrees_eq_twice_card_edges` 📖	mathematical	`IsBipartiteWith` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.sum` `Nat.instAddCommMonoid` `Finset` `Finset.instUnion` `degree` `neighborSetFintype` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype`	—	`isBipartiteWith_support_subset` `Finset.sum_subset` `Set.toFinset_subset` `Finset.coe_union` `degree_eq_zero_iff_notMem_support` `Set.mem_toFinset` `sum_degrees_support_eq_twice_card_edges`
`isBipartiteWith_support_subset` 📖	mathematical	`IsBipartiteWith`	`Set` `Set.instHasSubset` `support` `Set.instUnion`	—	`IsBipartiteWith.mem_of_adj`
`isBipartite_bipartiteDoubleCover` 📖	mathematical	—	`IsBipartite` `bipartiteDoubleCover`	—	`IsBipartiteWith.isBipartite` `isBipartiteWith_bipartiteDoubleCover`
`isBipartite_iff_exists_isBipartiteWith` 📖	mathematical	—	`IsBipartite` `Set` `IsBipartiteWith`	—	`IsBipartite.exists_isBipartiteWith` `IsBipartiteWith.isBipartite`
`neighborFinset_subset_between_union` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike`	`Finset` `Finset.instHasSubset` `neighborFinset` `neighborSetFintype` `Finset.instUnion` `between` `SetLike.coe` `Finset.instSetLike` `Compl.compl` `Set` `Set.instCompl` `instDecidableRelAdjBetweenOfDecidablePredMemSet` `Finset.decidableMem'` `Set.decidableCompl`	—	`Finset.coe_union` `Set.coe_toFinset` `neighborSet_subset_between_union`
`neighborFinset_subset_between_union_compl` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	`Finset` `Finset.instHasSubset` `neighborFinset` `neighborSetFintype` `Finset.instUnion` `between` `SetLike.coe` `Finset.instSetLike` `Compl.compl` `Set` `Set.instCompl` `instDecidableRelAdjBetweenOfDecidablePredMemSet` `Finset.decidableMem'` `Set.decidableCompl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	—	`Finset.coe_union` `Set.coe_toFinset` `Finset.coe_compl` `neighborSet_subset_between_union_compl`
`neighborSet_subset_between_union` 📖	mathematical	`Set` `Set.instMembership`	`Set` `Set.instHasSubset` `neighborSet` `Set.instUnion` `between` `Compl.compl` `Set.instCompl`	—	`neighborSet.eq_1` `Set.mem_union` `Set.mem_setOf` `between_adj`
`neighborSet_subset_between_union_compl` 📖	mathematical	`Set` `Set.instMembership` `Compl.compl` `Set.instCompl`	`Set` `Set.instHasSubset` `neighborSet` `Set.instUnion` `between` `Compl.compl` `Set.instCompl`	—	`neighborSet.eq_1` `Set.mem_union` `Set.mem_setOf` `between_adj`

SimpleGraph.Copy

Definitions

Name	Category	Theorems
`completeBipartiteGraph` 📖	CompOp	—

SimpleGraph.IsBipartite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isBipartiteWith` 📖	mathematical	—	`Set` `SimpleGraph.IsBipartiteWith`	—	`Fin.instNeZeroHAddNatOfNat_mathlib_1`
`subgraph` 📖	mathematical	—	`SimpleGraph.IsBipartite` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe`	—	`SimpleGraph.isBipartite_iff_exists_isBipartiteWith` `SimpleGraph.IsBipartiteWith.subgraph`

SimpleGraph.IsBipartiteWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint` 📖	mathematical	`SimpleGraph.IsBipartiteWith`	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`isBipartite` 📖	mathematical	`SimpleGraph.IsBipartiteWith`	`SimpleGraph.IsBipartite`	—	`mem_of_adj` `Disjoint.subset_compl_left` `disjoint` `Set.indicator_of_mem` `Set.indicator_of_notMem` `Fin.instNeZeroHAddNatOfNat_mathlib_1`
`mem_of_adj` 📖	mathematical	`SimpleGraph.IsBipartiteWith` `SimpleGraph.Adj`	`Set` `Set.instMembership`	—	—
`mem_of_mem_adj` 📖	mathematical	`SimpleGraph.IsBipartiteWith` `Set` `Set.instMembership` `SimpleGraph.Adj`	`Set` `Set.instMembership`	—	`Set.disjoint_left` `disjoint` `mem_of_adj`
`mem_of_mem_adj'` 📖	mathematical	`SimpleGraph.IsBipartiteWith` `Set` `Set.instMembership` `SimpleGraph.Adj`	`Set` `Set.instMembership`	—	`Set.disjoint_right` `disjoint` `mem_of_adj`
`subgraph` 📖	mathematical	`SimpleGraph.IsBipartiteWith`	`SimpleGraph.IsBipartiteWith` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe` `setOf` `Set` `Set.instMembership`	—	`mem_of_adj` `SimpleGraph.Subgraph.adj_sub`

---

← Back to Index