Documentation Verification Report

Matching

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

Statistics

Metric	Count
Definitions `IsAlternating`, `IsCycles`, `IsMatchingFree`, `IsMatching`, `toEdge`, `IsPerfectMatching`	6
Theorems `even_card_of_isPerfectMatching`, `odd_matches_node_outside`, `mono`, `spanningCoe`, `sup_edge`, `even_iff_exists_isMatching`, `existsUnique_ne_adj`, `exists_cycle_toSubgraph_verts_eq_connectedComponentSupp`, `other_adj_of_adj`, `reachable_deleteEdges`, `reachable_sdiff_toSubgraph_spanningCoe`, `snd_of_mem_support_of_isPath_of_adj`, `toSimpleGraph`, `mono`, `coeSubgraph`, `eq_of_adj_left`, `eq_of_adj_right`, `even_card`, `exists_of_disjoint_sets_of_equiv`, `iSup`, `induce_connectedComponent`, `map`, `map_ofLE`, `not_adj_left_of_ne`, `not_adj_right_of_ne`, `subgraphOfAdj`, `sup`, `support_eq_verts`, `surjective`, `toEdge_eq_of_adj`, `toEdge_eq_toEdge_of_adj`, `even_card`, `induce_connectedComponent_isMatching`, `isAlternating_symmDiff_left`, `isAlternating_symmDiff_right`, `symmDiff_isCycles`, `symmDiff_of_isAlternating`, `toSubgraph_iff`, `isMatching_map`, `isMatching_iff_forall_degree`, `isPerfectMatching_iff`, `isPerfectMatching_iff_forall_degree`, `adj_toSubgraph_iff_of_isCycles`, `isCycles_spanningCoe_toSubgraph`, `isCycles_spanningCoe_toSubgraph_sup_edge`, `exists_maximal_isMatchingFree`	46
Total	52

SimpleGraph

Definitions

Name	Category	Theorems
`IsAlternating` 📖	MathDef	2 math math: `Subgraph.IsPerfectMatching.isAlternating_symmDiff_left`, `Subgraph.IsPerfectMatching.isAlternating_symmDiff_right`
`IsCycles` 📖	MathDef	3 math math: `Walk.IsCycle.isCycles_spanningCoe_toSubgraph`, `Subgraph.IsPerfectMatching.symmDiff_isCycles`, `Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge`
`IsMatchingFree` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_maximal_isMatchingFree` 📖	mathematical	`IsMatchingFree`	`SimpleGraph` `instLE` `Subgraph.IsPerfectMatching`	—	`not_forall_not` `Finite.exists_le_maximal` `instFinite` `Maximal.prop` `Maximal.not_prop_of_gt`

SimpleGraph.ConnectedComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_card_of_isPerfectMatching` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`Even` `Fintype.card` `Set.Elem` `supp` `Subtype.fintype` `Set` `Set.instMembership` `SimpleGraph.instDecidableMemSupp`	—	`Fintype.card_ofFinset` `Set.toFinset_card` `SimpleGraph.Subgraph.IsMatching.even_card` `SimpleGraph.Subgraph.IsPerfectMatching.induce_connectedComponent_isMatching`
`odd_matches_node_outside` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`Set` `Set.instMembership` `SimpleGraph.Subgraph.Adj` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.deleteVerts` `Top.top` `SimpleGraph.Subgraph` `SimpleGraph.Subgraph.instTop` `Set.Elem` `supp` `SimpleGraph.Subgraph.coe` `SimpleGraph.ConnectedComponent` `SimpleGraph.oddComponents`	—	`Mathlib.Tactic.Push.not_and_eq` `mem_coe_supp_of_adj` `SimpleGraph.Subgraph.adj_sub` `Nat.not_even_iff_odd` `Subtype.prop` `Subtype.finite` `Nat.card_eq_fintype_card` `Set.toFinset_congr` `Set.image_congr` `Set.toFinset_image` `Finset.card_image_of_injective` `Set.toFinset_card` `SimpleGraph.Subgraph.IsMatching.even_card`

SimpleGraph.IsAlternating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`SimpleGraph.IsAlternating` `SimpleGraph` `SimpleGraph.instLE`	—	—	—
`spanningCoe` 📖	mathematical	`SimpleGraph.IsAlternating`	`SimpleGraph.Subgraph.spanningCoe`	—	`SimpleGraph.Subgraph.Adj.adj_sub`
`sup_edge` 📖	mathematical	`SimpleGraph.IsAlternating` `SimpleGraph.Adj`	`SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge`	—	`SimpleGraph.sup_edge_of_adj` `SimpleGraph.adj_congr_of_sym2` `SimpleGraph.Adj.symm`

SimpleGraph.IsClique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_iff_exists_isMatching` 📖	mathematical	`SimpleGraph.IsClique`	`Even` `Set.ncard` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.IsMatching`	—	`Set.exists_union_disjoint_ncard_eq_of_even` `Cardinal.eq` `Set.cast_ncard` `Set.finite_union` `SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv` `Disjoint.ne_of_mem` `Set.ncard_eq_toFinset_card` `SimpleGraph.Subgraph.IsMatching.even_card`

SimpleGraph.IsCycles

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique_ne_adj` 📖	mathematical	`SimpleGraph.IsCycles` `SimpleGraph.Adj`	`ExistsUnique`	—	`other_adj_of_adj` `Set.ncard_eq_two`
`exists_cycle_toSubgraph_verts_eq_connectedComponentSupp` 📖	mathematical	`SimpleGraph.IsCycles` `Set` `Set.instMembership` `SimpleGraph.ConnectedComponent.supp` `Set.Nonempty` `SimpleGraph.neighborSet`	`SimpleGraph.Walk.IsCycle` `SimpleGraph.Subgraph.verts` `SimpleGraph.Walk.toSubgraph`	—	`SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle` `reachable_deleteEdges` `SimpleGraph.Walk.fst_mem_support_of_mem_edges` `SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSupp` `SimpleGraph.Walk.toSubgraph_connected` `SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv` `Set.Nonempty.mono` `SimpleGraph.Subgraph.neighborSet_subset` `Set.nonempty_of_ncard_ne_zero` `SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two` `SimpleGraph.Walk.mem_verts_toSubgraph` `Cardinal.eq` `Set.cast_ncard` `Set.toFinite` `Subtype.finite` `SimpleGraph.Walk.IsCycle.rotate` `SimpleGraph.Walk.toSubgraph_rotate` `SimpleGraph.Walk.verts_toSubgraph`
`other_adj_of_adj` 📖	—	`SimpleGraph.IsCycles` `SimpleGraph.Adj`	—	—	`Set.exists_ne_of_one_lt_ncard`
`reachable_deleteEdges` 📖	mathematical	`SimpleGraph.Adj` `SimpleGraph.IsCycles`	`SimpleGraph.Reachable` `SimpleGraph.deleteEdges` `Sym2` `Set` `Set.instSingletonSet`	—	`sup_of_le_left` `SimpleGraph.Subgraph.spanningCoe_subgraphOfAdj` `SimpleGraph.Reachable.symm` `reachable_sdiff_toSubgraph_spanningCoe` `SimpleGraph.Walk.IsPath.of_adj`
`reachable_sdiff_toSubgraph_spanningCoe` 📖	mathematical	`SimpleGraph.IsCycles` `SimpleGraph.Walk.IsPath`	`SimpleGraph.Reachable` `SimpleGraph` `SimpleGraph.sdiff` `SimpleGraph.Subgraph.spanningCoe` `SimpleGraph.Walk.toSubgraph`	—	—
`snd_of_mem_support_of_isPath_of_adj` 📖	mathematical	`SimpleGraph.IsCycles` `SimpleGraph.Walk.support` `SimpleGraph.Walk.IsPath` `SimpleGraph.Adj`	`SimpleGraph.Walk.snd`	—	`SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj` `SimpleGraph.Walk.mem_support_iff_exists_getVert` `SimpleGraph.Walk.getVert_zero` `SimpleGraph.Walk.getVert_length` `Cardinal.eq` `Set.cast_ncard` `Set.toFinite` `Subtype.finite` `SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two` `Set.nonempty_of_mem` `SimpleGraph.Adj.symm` `SimpleGraph.Subgraph.adj_comm` `SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv`
`toSimpleGraph` 📖	mathematical	`SimpleGraph.IsCycles`	`SimpleGraph.spanningCoe` `SetLike.coe` `SimpleGraph.ConnectedComponent` `SimpleGraph.ConnectedComponent.instSetLike` `SimpleGraph.ConnectedComponent.toSimpleGraph`	—	`SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph` `SimpleGraph.mem_neighborSet` `Set.ext`

SimpleGraph.IsMatchingFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsMatchingFree`	—	—	`SimpleGraph.Subgraph.IsMatching.map_ofLE` `Set.image_congr` `Set.image_id'`

SimpleGraph.Subgraph

Definitions

Name	Category	Theorems
`IsMatching` 📖	MathDef	8 math math: `IsPerfectMatching.induce_connectedComponent_isMatching`, `SimpleGraph.IsClique.even_iff_exists_isMatching`, `IsMatching.exists_of_disjoint_sets_of_equiv`, `IsMatching.exists_of_universalVerts`, `isMatching_iff_forall_degree`, `IsMatching.subgraphOfAdj`, `SimpleGraph.exists_isMatching_of_forall_ncard_le`, `Iso.isMatching_map`
`IsPerfectMatching` 📖	MathDef	7 math math: `isPerfectMatching_iff`, `SimpleGraph.exists_maximal_isMatchingFree`, `IsPerfectMatching.toSubgraph_iff`, `isPerfectMatching_iff_forall_degree`, `IsPerfectMatching.exists_of_isClique_supp`, `SimpleGraph.exists_isPerfectMatching_of_forall_ncard_le`, `SimpleGraph.tutte`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMatching_iff_forall_degree` 📖	mathematical	—	`IsMatching` `degree`	—	—
`isPerfectMatching_iff` 📖	mathematical	—	`IsPerfectMatching` `ExistsUnique` `Adj`	—	`edge_vert`
`isPerfectMatching_iff_forall_degree` 📖	mathematical	—	`IsPerfectMatching` `degree`	—	—

SimpleGraph.Subgraph.IsMatching

Definitions

Name	Category	Theorems
`toEdge` 📖	CompOp	3 math math: `toEdge_eq_of_adj`, `toEdge_eq_toEdge_of_adj`, `toEdge.surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeSubgraph` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `Set.Elem` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.coe`	`SimpleGraph.Subgraph.coeSubgraph`	—	`Set.image_val_subset` `SimpleGraph.Subgraph.verts_coeSubgraph` `Set.mem_of_mem_image_val` `Set.mem_image` `Subtype.coe_eta` `SimpleGraph.Subgraph.coeSubgraph_adj`
`eq_of_adj_left` 📖	—	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.Adj`	—	—	`ExistsUnique.unique` `SimpleGraph.Subgraph.edge_vert`
`eq_of_adj_right` 📖	—	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.Adj`	—	—	`eq_of_adj_left` `SimpleGraph.Subgraph.Adj.symm`
`even_card` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching`	`Even` `Finset.card` `Set.toFinset` `SimpleGraph.Subgraph.verts`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `SimpleGraph.sum_degrees_eq_twice_card_edges` `Set.toFinset_card` `Finset.sum_congr` `SimpleGraph.Subgraph.coe_degree` `SimpleGraph.Subgraph.isMatching_iff_forall_degree` `Finset.sum_const` `mul_one`
`exists_of_disjoint_sets_of_equiv` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SimpleGraph.Adj` `Set.instMembership` `DFunLike.coe` `Equiv` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike`	`SimpleGraph.Subgraph.verts` `Set.instUnion` `SimpleGraph.Subgraph.IsMatching`	—	`SimpleGraph.Adj.symm` `Disjoint.ne_of_mem` `Subtype.coe_prop` `Subtype.coe_eta` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply`
`iSup` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `Pairwise` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SimpleGraph.Subgraph.support`	`iSup` `SimpleGraph.Subgraph` `SimpleGraph.Subgraph.instSupSet`	—	`Set.mem_iUnion` `SimpleGraph.Subgraph.verts_iSup` `SimpleGraph.Subgraph.iSup_adj` `SimpleGraph.Subgraph.mem_support`
`induce_connectedComponent` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching`	`SimpleGraph.Subgraph.induce` `Set` `Set.instInter` `SimpleGraph.Subgraph.verts` `SimpleGraph.ConnectedComponent.supp`	—	`SimpleGraph.Subgraph.edge_vert` `SimpleGraph.Subgraph.Adj.symm` `SimpleGraph.Adj.reachable` `SimpleGraph.Adj.symm` `SimpleGraph.Subgraph.adj_sub`
`map` 📖	mathematical	`DFunLike.coe` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.Subgraph.IsMatching`	`SimpleGraph.Subgraph.map`	—	—
`map_ofLE` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph` `SimpleGraph.instLE`	`SimpleGraph.Subgraph.map` `SimpleGraph.Hom.ofLE`	—	`Set.mem_image` `Relation.map_id_id`
`not_adj_left_of_ne` 📖	—	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.Adj`	—	—	`eq_of_adj_left`
`not_adj_right_of_ne` 📖	—	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.Adj`	—	—	`eq_of_adj_right`
`subgraphOfAdj` 📖	mathematical	`SimpleGraph.Adj`	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.subgraphOfAdj`	—	`Set.mem_singleton_iff` `Set.mem_insert_iff` `SimpleGraph.subgraphOfAdj_verts`
`sup` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SimpleGraph.Subgraph.support`	`SimpleGraph.Subgraph` `SimpleGraph.Subgraph.instMax`	—	`SimpleGraph.Subgraph.sup_adj` `SimpleGraph.Subgraph.mem_support` `Set.disjoint_left` `Set.mem_or_mem_of_mem_union` `sup_comm` `Disjoint.symm`
`support_eq_verts` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching`	`SimpleGraph.Subgraph.support` `SimpleGraph.Subgraph.verts`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `SimpleGraph.Subgraph.support_subset_verts`
`toEdge_eq_of_adj` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `Set` `Set.instMembership` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.Adj`	`toEdge` `Sym2` `SimpleGraph.Subgraph.edgeSet`	—	`SimpleGraph.Subgraph.edge_vert`
`toEdge_eq_toEdge_of_adj` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching` `Set` `Set.instMembership` `SimpleGraph.Subgraph.verts` `SimpleGraph.Subgraph.Adj`	`toEdge`	—	`toEdge_eq_of_adj` `SimpleGraph.Subgraph.symm` `Sym2.eq_swap`

SimpleGraph.Subgraph.IsMatching.toEdge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective` 📖	mathematical	`SimpleGraph.Subgraph.IsMatching`	`Set.Elem` `SimpleGraph.Subgraph.verts` `Sym2` `SimpleGraph.Subgraph.edgeSet` `SimpleGraph.Subgraph.IsMatching.toEdge`	—	`SimpleGraph.Subgraph.edge_vert` `SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj`

SimpleGraph.Subgraph.IsPerfectMatching

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_card` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`Even` `Fintype.card`	—	`SimpleGraph.Subgraph.IsSpanning.card_verts` `SimpleGraph.Subgraph.IsMatching.even_card`
`induce_connectedComponent_isMatching` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.induce` `SimpleGraph.ConnectedComponent.supp`	—	`SimpleGraph.Subgraph.IsSpanning.verts_eq_univ` `Set.univ_inter` `SimpleGraph.Subgraph.IsMatching.induce_connectedComponent`
`isAlternating_symmDiff_left` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`SimpleGraph.IsAlternating` `symmDiff` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sdiff` `SimpleGraph.Subgraph.spanningCoe`	—	—
`isAlternating_symmDiff_right` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`SimpleGraph.IsAlternating` `symmDiff` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sdiff` `SimpleGraph.Subgraph.spanningCoe`	—	`symmDiff_comm` `isAlternating_symmDiff_left`
`symmDiff_isCycles` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching`	`SimpleGraph.IsCycles` `symmDiff` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sdiff` `SimpleGraph.Subgraph.spanningCoe`	—	`Set.ext`
`symmDiff_of_isAlternating` 📖	mathematical	`SimpleGraph.Subgraph.IsPerfectMatching` `SimpleGraph.IsAlternating` `SimpleGraph.Subgraph.spanningCoe` `SimpleGraph.IsCycles`	`symmDiff` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.sdiff` `Top.top` `SimpleGraph.Subgraph` `SimpleGraph.Subgraph.instTop`	—	`SimpleGraph.Subgraph.isPerfectMatching_iff` `SimpleGraph.IsCycles.other_adj_of_adj`
`toSubgraph_iff` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.Subgraph.spanningCoe`	`SimpleGraph.Subgraph.IsPerfectMatching` `SimpleGraph.toSubgraph`	—	—

SimpleGraph.Subgraph.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMatching_map` 📖	mathematical	—	`SimpleGraph.Subgraph.IsMatching` `SimpleGraph.Subgraph.map` `SimpleGraph.Iso.toHom`	—	`SimpleGraph.Iso.symm_toHom_comp_toHom` `SimpleGraph.Subgraph.map_id` `SimpleGraph.Subgraph.IsMatching.map` `RelIso.injective`

SimpleGraph.Walk.IsCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_toSubgraph_iff_of_isCycles` 📖	mathematical	`SimpleGraph.Walk.IsCycle` `SimpleGraph.IsCycles` `Set` `Set.instMembership` `SimpleGraph.Subgraph.verts` `SimpleGraph.Walk.toSubgraph`	`SimpleGraph.Subgraph.Adj` `SimpleGraph.Adj`	—	`SimpleGraph.Subgraph.adj_iff_of_neighborSet_equiv` `ncard_neighborSet_toSubgraph_eq_two` `SimpleGraph.Walk.verts_toSubgraph` `Cardinal.eq` `Set.cast_ncard` `Set.toFinite` `Finite.of_fintype` `SimpleGraph.Walk.finite_neighborSet_toSubgraph` `Set.Nonempty.mono` `SimpleGraph.Subgraph.neighborSet_subset` `Set.nonempty_of_ncard_ne_zero` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`isCycles_spanningCoe_toSubgraph` 📖	mathematical	`SimpleGraph.Walk.IsCycle`	`SimpleGraph.IsCycles` `SimpleGraph.Subgraph.spanningCoe` `SimpleGraph.Walk.toSubgraph`	—	`ncard_neighborSet_toSubgraph_eq_two` `SimpleGraph.Walk.mem_verts_toSubgraph` `SimpleGraph.Subgraph.edge_vert`

SimpleGraph.Walk.IsPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCycles_spanningCoe_toSubgraph_sup_edge` 📖	mathematical	`SimpleGraph.Walk.IsPath` `Sym2` `SimpleGraph.Walk.edges`	`SimpleGraph.IsCycles` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.Subgraph.spanningCoe` `SimpleGraph.Walk.toSubgraph` `SimpleGraph.edge`	—	`OrderTop.le_top` `SimpleGraph.ext` `SimpleGraph.Walk.IsCycle.isCycles_spanningCoe_toSubgraph` `SimpleGraph.Walk.edges_map` `Sym2.map_id`

---

← Back to Index