Documentation Verification Report

WalkCounting

📁 Source: Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

Statistics

Metric	Count
Definitions `instFintype`, `finsetWalkLength`, `finsetWalkLengthLT`, `fintypeSetPathLength`, `fintypeSetPathLengthLT`, `fintypeSetWalkLength`, `fintypeSetWalkLengthLT`, `fintypeSubtypePathLength`, `fintypeSubtypePathLengthLT`, `fintypeSubtypeWalkLength`, `fintypeSubtypeWalkLengthLT`, `instDecidableConnected`, `instDecidableMemSupp`, `instDecidablePreconnected`, `instDecidableRelReachable`, `instFintypeConnectedComponent`, `oddComponents`, `walkLengthTwoEquivCommonNeighbors`	18
Theorems `card_le_card_of_le`, `odd_oddComponents_ncard_subset_supp`, `card_set_walk_length_eq`, `coe_finsetWalkLengthLT_eq`, `coe_finsetWalkLength_eq`, `disjiUnion_supp_toFinset_eq_supp_toFinset`, `mem_finsetWalkLengthLT_iff`, `mem_finsetWalkLength_iff`, `ncard_oddComponents_mono`, `odd_ncard_oddComponents`, `reachable_iff_exists_finsetWalkLength_nonempty`, `set_walk_length_succ_eq`, `set_walk_length_toFinset_eq`, `set_walk_length_zero_eq_of_ne`, `set_walk_self_length_zero_eq`, `walkLengthTwoEquivCommonNeighbors_apply_coe`, `walkLengthTwoEquivCommonNeighbors_symm_apply_coe`	17
Total	35

SimpleGraph

Definitions

Name	Category	Theorems
`finsetWalkLength` 📖	CompOp	5 math math: `card_set_walk_length_eq`, `reachable_iff_exists_finsetWalkLength_nonempty`, `mem_finsetWalkLength_iff`, `coe_finsetWalkLength_eq`, `set_walk_length_toFinset_eq`
`finsetWalkLengthLT` 📖	CompOp	2 math math: `mem_finsetWalkLengthLT_iff`, `coe_finsetWalkLengthLT_eq`
`fintypeSetPathLength` 📖	CompOp	—
`fintypeSetPathLengthLT` 📖	CompOp	—
`fintypeSetWalkLength` 📖	CompOp	3 math math: `card_set_walk_length_eq`, `adjMatrix_pow_apply_eq_card_walk`, `set_walk_length_toFinset_eq`
`fintypeSetWalkLengthLT` 📖	CompOp	—
`fintypeSubtypePathLength` 📖	CompOp	—
`fintypeSubtypePathLengthLT` 📖	CompOp	—
`fintypeSubtypeWalkLength` 📖	CompOp	—
`fintypeSubtypeWalkLengthLT` 📖	CompOp	—
`instDecidableConnected` 📖	CompOp	—
`instDecidableMemSupp` 📖	CompOp	2 math math: `disjiUnion_supp_toFinset_eq_supp_toFinset`, `ConnectedComponent.even_card_of_isPerfectMatching`
`instDecidablePreconnected` 📖	CompOp	—
`instDecidableRelReachable` 📖	CompOp	—
`instFintypeConnectedComponent` 📖	CompOp	2 math math: `card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix`, `disjiUnion_supp_toFinset_eq_supp_toFinset`
`oddComponents` 📖	CompOp	4 math math: `ncard_oddComponents_mono`, `ConnectedComponent.odd_matches_node_outside`, `odd_ncard_oddComponents`, `ConnectedComponent.odd_oddComponents_ncard_subset_supp`
`walkLengthTwoEquivCommonNeighbors` 📖	CompOp	2 math math: `walkLengthTwoEquivCommonNeighbors_symm_apply_coe`, `walkLengthTwoEquivCommonNeighbors_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_set_walk_length_eq` 📖	mathematical	—	`Fintype.card` `Set.Elem` `Walk` `setOf` `Walk.length` `fintypeSetWalkLength` `Finset.card` `finsetWalkLength`	—	`Fintype.card_ofFinset` `Finset.mem_coe` `coe_finsetWalkLength_eq`
`coe_finsetWalkLengthLT_eq` 📖	mathematical	—	`SetLike.coe` `Finset` `Walk` `Finset.instSetLike` `finsetWalkLengthLT` `setOf` `Walk.length`	—	`Set.ext` `Finset.disjiUnion_eq_biUnion` `Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_range`
`coe_finsetWalkLength_eq` 📖	mathematical	—	`SetLike.coe` `Finset` `Walk` `Finset.instSetLike` `finsetWalkLength` `setOf` `Walk.length`	—	`eq_or_ne` `Finset.coe_singleton` `Finset.coe_empty` `set_walk_length_zero_eq_of_ne` `Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_map` `Set.iUnion_true` `Set.iUnion_coe_set` `Set.image_congr` `set_walk_length_succ_eq`
`disjiUnion_supp_toFinset_eq_supp_toFinset` 📖	mathematical	`SimpleGraph` `instLE`	`Finset.disjiUnion` `ConnectedComponent` `Finset.filter` `Set` `Set.instHasSubset` `ConnectedComponent.supp` `Finset.univ` `instFintypeConnectedComponent` `Set.toFinset` `Subtype.fintype` `Set.instMembership` `instDecidableMemSupp`	—	`Finset.coe_injective` `Finset.disjiUnion_eq_biUnion` `Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_filter` `Set.coe_toFinset` `ConnectedComponent.biUnion_supp_eq_supp`
`mem_finsetWalkLengthLT_iff` 📖	mathematical	—	`Walk` `Finset` `Finset.instMembership` `finsetWalkLengthLT` `Walk.length`	—	`Set.ext_iff` `coe_finsetWalkLengthLT_eq`
`mem_finsetWalkLength_iff` 📖	mathematical	—	`Walk` `Finset` `Finset.instMembership` `finsetWalkLength` `Walk.length`	—	`Set.ext_iff` `coe_finsetWalkLength_eq`
`ncard_oddComponents_mono` 📖	mathematical	`SimpleGraph` `instLE`	`Set.ncard` `ConnectedComponent` `oddComponents`	—	`Set.nonempty_of_ncard_ne_zero` `ConnectedComponent.odd_oddComponents_ncard_subset_supp` `Nat.card_le_card_of_injective` `Subtype.finite` `ConnectedComponent.instFinite` `Subtype.val_injective` `ConnectedComponent.eq_of_common_vertex` `ConnectedComponent.nonempty_supp` `Set.Nonempty.some_mem`
`odd_ncard_oddComponents` 📖	mathematical	—	`Odd` `Nat.instSemiring` `Set.ncard` `ConnectedComponent` `oddComponents` `Nat.card`	—	`nonempty_fintype` `Nat.card_eq_fintype_card` `set_fintype_card_eq_univ_iff` `iUnion_connectedComponentSupp` `Set.toFinset_iUnion` `Finset.card_biUnion` `Set.disjoint_toFinset` `pairwise_disjoint_supp_connectedComponent` `Finset.sum_congr` `Set.ncard_coe_finset` `Finset.odd_sum_iff_odd_card_odd`
`reachable_iff_exists_finsetWalkLength_nonempty` 📖	mathematical	—	`Reachable` `Finset.Nonempty` `Walk` `finsetWalkLength` `neighborSetFintype` `Fintype.card`	—	`Reachable.elim_path` `Walk.IsPath.length_lt` `Path.isPath`
`set_walk_length_succ_eq` 📖	mathematical	—	`setOf` `Walk` `Walk.length` `Set.iUnion` `Adj` `Set.image` `Walk.cons`	—	`Set.ext` `Set.iUnion_congr_Prop` `AddRightCancelSemigroup.toIsRightCancelAdd`
`set_walk_length_toFinset_eq` 📖	mathematical	—	`Set.toFinset` `Walk` `setOf` `Walk.length` `fintypeSetWalkLength` `finsetWalkLength`	—	`Set.toFinset_congr` `Finset.toFinset_coe`
`set_walk_length_zero_eq_of_ne` 📖	mathematical	—	`setOf` `Walk` `Walk.length` `Set` `Set.instEmptyCollection`	—	`Set.ext` `Walk.eq_of_length_eq_zero`
`set_walk_self_length_zero_eq` 📖	mathematical	—	`setOf` `Walk` `Walk.length` `Set` `Set.instSingletonSet` `Walk.nil`	—	—
`walkLengthTwoEquivCommonNeighbors_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `commonNeighbors` `DFunLike.coe` `Equiv` `Walk` `Walk.length` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `walkLengthTwoEquivCommonNeighbors` `Walk.snd`	—	—
`walkLengthTwoEquivCommonNeighbors_symm_apply_coe` 📖	mathematical	—	`Walk` `Walk.length` `DFunLike.coe` `Equiv` `Set.Elem` `commonNeighbors` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `walkLengthTwoEquivCommonNeighbors` `Walk.concat` `Set` `Set.instMembership` `Adj.toWalk`	—	—

SimpleGraph.ConnectedComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_of_le` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`Nat.card` `SimpleGraph.ConnectedComponent`	—	`Nat.card_le_card_of_surjective` `instFinite` `surjective_map_ofLE`
`odd_oddComponents_ncard_subset_supp` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`Odd` `Nat.instSemiring` `Set.ncard` `SimpleGraph.ConnectedComponent` `setOf` `Set` `Set.instMembership` `SimpleGraph.oddComponents` `Set.instHasSubset` `supp`	—	`nonempty_fintype` `Nat.card_eq_card_toFinset` `SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset` `Finset.card_disjiUnion` `Finset.sum_congr` `Set.toFinset_card` `Fintype.card_ofFinset` `Finset.odd_sum_iff_odd_card_odd` `Nat.card_eq_fintype_card` `Finset.ext` `Finset.filter.congr_simp` `Set.toFinset_setOf` `Finset.coe_filter`

SimpleGraph.Path

Definitions

Name	Category	Theorems
`instFintype` 📖	CompOp	—

---

← Back to Index