Documentation Verification Report

Trails

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

Statistics

Metric	Count
Definitions `IsEulerian`, `fintypeEdgeSet`, `edgesFinset`	3
Theorems `card_filter_odd_degree`, `card_odd_degree`, `edgeSet_eq`, `edgesFinset_eq`, `even_degree_iff`, `isTrail`, `mem_edges_iff`, `even_countP_edges_iff`, `isEulerian_iff`, `isEulerian_of_forall_mem`, `isEulerian_iff`	11
Total	14

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`IsEulerian` 📖	MathDef	3 math math: `isEulerian_iff`, `IsTrail.isEulerian_iff`, `IsTrail.isEulerian_of_forall_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEulerian_iff` 📖	mathematical	—	`IsEulerian` `IsTrail` `Sym2` `edges`	—	`IsEulerian.isTrail` `IsEulerian.mem_edges_iff` `IsTrail.isEulerian_of_forall_mem`

SimpleGraph.Walk.IsEulerian

Definitions

Name	Category	Theorems
`fintypeEdgeSet` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_filter_odd_degree` 📖	mathematical	`SimpleGraph.Walk.IsEulerian` `Finset.filter` `Odd` `Nat.instSemiring` `SimpleGraph.degree` `SimpleGraph.neighborSetFintype` `Nat.instDecidablePredOdd` `Finset.univ`	`Finset.card`	—	`Finset.filter.congr_simp` `even_degree_iff` `eq_or_ne` `Finset.filter_false` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.card_insert_of_notMem` `Finset.card_singleton` `Finset.ext`
`card_odd_degree` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`Fintype.card` `Set.Elem` `setOf` `Odd` `Nat.instSemiring` `SimpleGraph.degree` `SimpleGraph.neighborSetFintype` `Subtype.fintype` `Set` `Set.instMembership` `Set.decidableSetOf` `Nat.instDecidablePredOdd`	—	`Set.toFinset_card` `card_filter_odd_degree` `Set.toFinset_setOf`
`edgeSet_eq` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`SimpleGraph.Walk.edgeSet` `SimpleGraph.edgeSet`	—	`SimpleGraph.Walk.IsTrail.isEulerian_iff` `isTrail`
`edgesFinset_eq` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`SimpleGraph.Walk.IsTrail.edgesFinset` `isTrail` `SimpleGraph.edgeFinset`	—	`Finset.ext` `isTrail` `SimpleGraph.Walk.IsTrail.edges_nodup` `mem_edges_iff`
`even_degree_iff` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`Even` `SimpleGraph.degree` `SimpleGraph.neighborSetFintype`	—	`Multiset.coe_countP` `Multiset.countP_eq_card_filter` `SimpleGraph.card_incidenceFinset_eq_degree` `isTrail` `edgesFinset_eq` `SimpleGraph.incidenceFinset_eq_filter` `SimpleGraph.Walk.IsTrail.even_countP_edges_iff`
`isTrail` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`SimpleGraph.Walk.IsTrail`	—	`SimpleGraph.Walk.isTrail_def` `List.nodup_iff_count_le_one` `Eq.le` `SimpleGraph.Walk.edges_subset_edgeSet`
`mem_edges_iff` 📖	mathematical	`SimpleGraph.Walk.IsEulerian`	`Sym2` `SimpleGraph.Walk.edges` `Set` `Set.instMembership` `SimpleGraph.edgeSet`	—	`SimpleGraph.Walk.edges_subset_edgeSet` `Eq.ge`

SimpleGraph.Walk.IsTrail

Definitions

Name	Category	Theorems
`edgesFinset` 📖	CompOp	1 math math: `SimpleGraph.Walk.IsEulerian.edgesFinset_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_countP_edges_iff` 📖	mathematical	`SimpleGraph.Walk.IsTrail`	`Even` `Sym2` `SetLike.instMembership` `Sym2.instSetLike` `Sym2.Mem.decidable` `SimpleGraph.Walk.edges`	—	`instIsEmptyFalse` `Nat.even_add_one` `SimpleGraph.Walk.isTrail_cons` `SimpleGraph.Adj.ne` `SimpleGraph.loopless`
`isEulerian_iff` 📖	mathematical	`SimpleGraph.Walk.IsTrail`	`SimpleGraph.Walk.IsEulerian` `SimpleGraph.Walk.edgeSet` `SimpleGraph.edgeSet`	—	`Set.Subset.antisymm` `SimpleGraph.Walk.edges_subset_edgeSet` `SimpleGraph.Walk.isEulerian_iff`
`isEulerian_of_forall_mem` 📖	mathematical	`SimpleGraph.Walk.IsTrail` `Sym2` `SimpleGraph.Walk.edges`	`SimpleGraph.Walk.IsEulerian`	—	`List.count_eq_one_of_mem` `edges_nodup`

---

← Back to Index