Documentation Verification Report

Counting

📁 Source: Mathlib/Combinatorics/SimpleGraph/Walks/Counting.lean

Statistics

Metric	Count
Definitions `instFintype`, `finsetWalkLength`, `finsetWalkLengthLT`, `fintypeSetPathLength`, `fintypeSetPathLengthLT`, `fintypeSetWalkLength`, `fintypeSetWalkLengthLT`, `fintypeSubtypePathLength`, `fintypeSubtypePathLengthLT`, `fintypeSubtypeWalkLength`, `fintypeSubtypeWalkLengthLT`, `walkLengthTwoEquivCommonNeighbors`	12
Theorems `card_set_walk_length_eq`, `coe_finsetWalkLengthLT_eq`, `coe_finsetWalkLength_eq`, `mem_finsetWalkLengthLT_iff`, `mem_finsetWalkLength_iff`, `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`	11
Total	23

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	—
`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`
`mem_finsetWalkLengthLT_iff` 📖	mathematical	—	`Walk` `Finset` `SetLike.instMembership` `Finset.instSetLike` `finsetWalkLengthLT` `Walk.length`	—	`Set.ext_iff` `coe_finsetWalkLengthLT_eq`
`mem_finsetWalkLength_iff` 📖	mathematical	—	`Walk` `Finset` `SetLike.instMembership` `Finset.instSetLike` `finsetWalkLength` `Walk.length`	—	`Set.ext_iff` `coe_finsetWalkLength_eq`
`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.Path

Definitions

Name	Category	Theorems
`instFintype` 📖	CompOp	—

---

← Back to Index