Documentation Verification Report

Dart

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

Statistics

Metric	Count
Definitions `Dart`, `edge`, `fintype`, `toProd`, `DartAdj`, `dartOfNeighborSet`, `instDecidableEqDart`, `decEq`	8
Theorems `adj`, `edge_comp_symm`, `edge_mem`, `edge_mk`, `edge_symm`, `ext`, `ext_iff`, `fst_ne_snd`, `snd_ne_fst`, `symm_involutive`, `symm_mk`, `symm_ne`, `symm_symm`, `symm_toProd`, `toProd_injective`, `dartOfNeighborSet_injective`, `dartOfNeighborSet_toProd`, `dart_edge_eq_iff`, `dart_edge_eq_mk'_iff`, `dart_edge_eq_mk'_iff'`, `nonempty_dart_top`	21
Total	29

SimpleGraph

Definitions

Name	Category	Theorems
`Dart` 📖	CompData	54 math math: `Walk.lastDart_eq_getLast_darts`, `Walk.exists_boundary_dart`, `Walk.darts_take`, `Walk.head_darts_fst`, `Dart.edge_fiber`, `Walk.mem_darts_iff_infix_support`, `dart_edge_fiber_card`, `Walk.darts_concat`, `Walk.firstDart_eq_head_darts`, `Walk.darts_injective`, `Walk.isSubwalk_toWalk_iff_mem_darts`, `Walk.mem_darts_reverse`, `Walk.firstDart_mem_darts`, `Walk.darts_map`, `Walk.darts_toPath_subset`, `Dart.symm_involutive`, `Walk.getLast_darts_snd`, `dart_card_eq_twice_card_edges`, `Walk.isChain_dartAdj_darts`, `Walk.darts_nodup_of_support_nodup`, `Walk.map_fst_darts_append`, `Walk.darts_drop`, `Walk.darts_reverse`, `dartOfNeighborSet_injective`, `Dart.edge_comp_symm`, `dart_fst_fiber`, `nonempty_dart_top`, `Walk.IsSubwalk.darts_subset`, `Walk.darts_cons`, `Walk.getLast_darts_eq_lastDart`, `dart_card_eq_sum_degrees`, `Walk.isSubwalk_iff_darts_isInfix`, `Walk.length_darts`, `dart_fst_fiber_card_eq_degree`, `Walk.IsSubwalk.darts_isInfix`, `Walk.chain'_dartAdj_darts`, `Walk.darts_append`, `Walk.darts_nil`, `Walk.chain_dartAdj_darts`, `Walk.darts_bypass_subset`, `Walk.toDeleteEdges_cons`, `Walk.mem_darts_iff_fst_snd_infix_support`, `Walk.map_snd_darts`, `Walk.cons_map_snd_darts`, `Walk.darts_eq_nil`, `Walk.lastDart_mem_darts`, `Walk.darts_dropUntil_subset`, `Walk.darts_takeUntil_subset`, `Dart.toProd_injective`, `Walk.isChain_dartAdj_cons_darts`, `Walk.map_fst_darts`, `Walk.head_darts_eq_firstDart`, `Walk.rotate_darts`, `Walk.isSubwalk_toWalk_adj_iff_mem_darts`
`DartAdj` 📖	MathDef	4 math math: `Walk.isChain_dartAdj_darts`, `Walk.chain'_dartAdj_darts`, `Walk.chain_dartAdj_darts`, `Walk.isChain_dartAdj_cons_darts`
`dartOfNeighborSet` 📖	CompOp	3 math math: `dartOfNeighborSet_injective`, `dart_fst_fiber`, `dartOfNeighborSet_toProd`
`instDecidableEqDart` 📖	CompOp	2 math math: `Dart.edge_fiber`, `dart_fst_fiber`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dartOfNeighborSet_injective` 📖	mathematical	—	`Set.Elem` `neighborSet` `Dart` `dartOfNeighborSet`	—	—
`dartOfNeighborSet_toProd` 📖	mathematical	—	`Dart.toProd` `dartOfNeighborSet` `Set` `Set.instMembership` `neighborSet`	—	—
`dart_edge_eq_iff` 📖	mathematical	—	`Dart.edge` `Dart.symm`	—	`Adj.symm`
`dart_edge_eq_mk'_iff` 📖	mathematical	—	`Dart.edge` `Dart.toProd`	—	—
`dart_edge_eq_mk'_iff'` 📖	mathematical	—	`Dart.edge` `Dart.toProd`	—	`dart_edge_eq_mk'_iff`
`nonempty_dart_top` 📖	mathematical	—	`Dart` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`exists_pair_ne`

SimpleGraph.Dart

Definitions

Name	Category	Theorems
`edge` 📖	CompOp	12 math math: `edge_mk`, `edge_fiber`, `SimpleGraph.dart_edge_fiber_card`, `SimpleGraph.Walk.edge_lastDart`, `SimpleGraph.dart_edge_eq_mk'_iff'`, `SimpleGraph.dart_edge_eq_iff`, `edge_symm`, `SimpleGraph.dart_edge_eq_mk'_iff`, `SimpleGraph.Walk.edge_firstDart`, `edge_comp_symm`, `edge_mem`, `SimpleGraph.Walk.toDeleteEdges_cons`
`fintype` 📖	CompOp	6 math math: `edge_fiber`, `SimpleGraph.dart_edge_fiber_card`, `SimpleGraph.dart_card_eq_twice_card_edges`, `SimpleGraph.dart_fst_fiber`, `SimpleGraph.dart_card_eq_sum_degrees`, `SimpleGraph.dart_fst_fiber_card_eq_degree`
`toProd` 📖	CompOp	25 math math: `SimpleGraph.Walk.exists_boundary_dart`, `SimpleGraph.Walk.head_darts_fst`, `SimpleGraph.Walk.snd_darts_getElem`, `SimpleGraph.Walk.lastDart_toProd`, `ext_iff`, `SimpleGraph.dart_edge_eq_mk'_iff'`, `SimpleGraph.Walk.getLast_darts_snd`, `SimpleGraph.Hom.mapDart_apply`, `SimpleGraph.dart_edge_eq_mk'_iff`, `SimpleGraph.Walk.map_fst_darts_append`, `SimpleGraph.Walk.firstDart_toProd`, `SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts`, `SimpleGraph.dart_fst_fiber`, `symm_toProd`, `SimpleGraph.dart_fst_fiber_card_eq_degree`, `SimpleGraph.dartOfNeighborSet_toProd`, `SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts`, `adj`, `SimpleGraph.Walk.mem_darts_iff_fst_snd_infix_support`, `SimpleGraph.Walk.fst_darts_getElem`, `SimpleGraph.Walk.map_snd_darts`, `SimpleGraph.Walk.cons_map_snd_darts`, `toProd_injective`, `SimpleGraph.Walk.map_fst_darts`, `SimpleGraph.Walk.isSubwalk_toWalk_adj_iff_mem_darts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj` 📖	mathematical	—	`SimpleGraph.Adj` `toProd`	—	—
`edge_comp_symm` 📖	mathematical	—	`SimpleGraph.Dart` `Sym2` `edge` `symm`	—	`edge_symm`
`edge_mem` 📖	mathematical	—	`Sym2` `Set` `Set.instMembership` `SimpleGraph.edgeSet` `edge`	—	`adj`
`edge_mk` 📖	mathematical	`SimpleGraph.Adj`	`edge`	—	—
`edge_symm` 📖	mathematical	—	`edge` `symm`	—	`Sym2.eq_swap`
`ext` 📖	—	`toProd`	—	—	`ext_iff`
`ext_iff` 📖	mathematical	—	`toProd`	—	—
`fst_ne_snd` 📖	—	—	—	—	`SimpleGraph.irrefl` `adj`
`snd_ne_fst` 📖	—	—	—	—	`SimpleGraph.irrefl` `adj`
`symm_involutive` 📖	mathematical	—	`Function.Involutive` `SimpleGraph.Dart` `symm`	—	`symm_symm`
`symm_mk` 📖	mathematical	`SimpleGraph.Adj`	`symm` `SimpleGraph.Adj.symm`	—	—
`symm_ne` 📖	—	—	—	—	`SimpleGraph.Adj.ne` `adj`
`symm_symm` 📖	mathematical	—	`symm`	—	`ext`
`symm_toProd` 📖	mathematical	—	`toProd` `symm`	—	—
`toProd_injective` 📖	mathematical	—	`SimpleGraph.Dart` `toProd`	—	`ext`

SimpleGraph.instDecidableEqDart

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index