Documentation Verification Report

Paths

πŸ“ Source: Mathlib/Combinatorics/SimpleGraph/Paths.lean

Statistics

MetricCount
DefinitionsPaths, map, mapEmbedding, nil, reverse, singleton, IsCircuit, IsCycle, IsPath, IsTrail, bypass, cycleBypass, instDecidableIsPathOfDecidableEq, toPath
14
Theoremscons_isCycle, count_edges_eq_one, count_support_eq_one, isPath, isTrail, loop_eq, mapEmbedding_coe, mapEmbedding_injective, map_coe, map_injective, mk'_mem_edges_singleton, nil_coe, nodup_support, notMem_edges_of_loop, reverse_coe, singleton_coe, isTrail, ne_nil, not_nil, rotate, toIsTrail, count_support, count_support_of_mem, getVert_endpoint_iff, getVert_injOn, getVert_injOn', getVert_sub_one_ne_getVert_add_one, isCircuit, isPath_of_append_left, isPath_of_append_right, isPath_tail, isPath_takeUntil, map, mapLe, ne_bot, not_nil, not_of_nil, of_mapLe, reverse, rotate, snd_ne_penultimate, support_nodup, three_le_length, toDeleteEdges, toIsCircuit, transfer, concat, cons, disjoint_support_of_append, dropUntil, eq_penultimate_of_mem_edges, eq_snd_of_mem_edges, getVert_eq_end_iff, getVert_eq_start_iff, getVert_injOn, getVert_injOn_iff, isTrail, length_lt, mapLe, mem_support_iff_exists_append, mk', ne_of_mem_support_of_append, nil, of_adj, of_append_left, of_append_right, of_cons, of_map, of_mapLe, reverse, support_nodup, tail, takeUntil, toDeleteEdges, toIsTrail, transfer, cons, count_edges_eq_one, count_edges_le_one, disjoint_edges_takeUntil_dropUntil, dropUntil, edges_nodup, isCycle_cycleBypass, length_le_card_edgeFinset, mapLe, nil, of_append_left, of_append_right, of_cons, of_mapLe, reverse, rotate, takeUntil, bypass_copy, bypass_eq_self_of_length_le, bypass_isPath, concat_isPath_iff, cons_isCycle_iff, cons_isPath_iff, cons_isTrail_iff, cycleBypass_nil, darts_bypass_subset, darts_toPath_subset, edges_bypass_subset, edges_cycleBypass_subset, edges_toPath_subset, endpoint_notMem_support_takeUntil, exists_isPath_forall_isPath_length_le_length, exists_isTrail_forall_isTrail_length_le_length, isCircuit_copy, isCircuit_def, isCycle_copy, isCycle_def, isCycle_iff_isPath_tail_and_le_length, isCycle_reverse, isPath_copy, isPath_def, isPath_iff_eq_nil, isPath_iff_injective_get_support, isPath_of_isSubwalk, isPath_reverse_iff, isTrail_cons, isTrail_copy, isTrail_def, isTrail_of_isSubwalk, length_bypass_le, mapLe_isCycle, mapLe_isPath, mapLe_isTrail, map_isCycle_iff_of_injective, map_isPath_iff_of_injective, map_isPath_of_injective, map_isTrail_iff_of_injective, map_isTrail_of_injective, not_nil_of_isCycle_cons, reverse_isTrail_iff, support_bypass_subset, support_toPath_subset, toDeleteEdges_copy
139
Total153

CategoryTheory

Definitions

NameCategoryTheorems
Paths πŸ“–CompOp
54 mathmath: Cat.freeMap_map, composePath_comp', Quiv.pathsOf_pathComposition_toPrefunctor, Localization.Construction.lift_obj, Cat.freeMap_obj, pathComposition_obj, Cat.freeMap_comp, Cat.freeMapIdIso_hom_app, Cat.free_map, Cat.FreeRefl.instFullPathsQuotientFunctor, Quiv.lift_obj, SSet.OneTruncationβ‚‚.HoRelβ‚‚.mk, ReflQuiv.adj.unit.map_app_eq, Paths.of_map, quotientPathsTo_obj, Localization.Construction.lift_map, FreeBicategory.preinclusion_mapβ‚‚, Quiv.adj_homEquiv, Cat.freeReflMap_naturality, Quiver.FreeGroupoid.congr_comp_reverse, Cat.FreeRefl.quotientFunctor_map_id, Cat.freeMap_id, Cat.FreeRefl.quotientFunctor_map_nil, Paths.lift_spec, Quiv.pathComposition_naturality, Cat.freeMapCompIso_hom_app, Cat.free_obj, Quiv.freeMap_pathsOf_pathComposition, FreeGroupoid.eq_mk, Quiv.lift_map, Paths.lift_cons, Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map, FreeBicategory.normalize_naturality, Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj, Localization.Construction.liftToPathCategory_map, ReflQuiv.adj.counit.comp_app_eq, toQuotientPaths_obj_as, composePath_id, Quiv.pathsOf_freeMap_toPrefunctor, Paths.lift_toPath, Quiver.FreeGroupoid.of_eq, Localization.Construction.objEquiv_symm_apply, Localization.Construction.liftToPathCategory_obj, Quiver.FreeGroupoid.congr_reverse_comp, FreeBicategory.preinclusion_obj, Paths.lift_nil, pathComposition_map, toQuotientPaths_map, Paths.of_obj, quotientPathsTo_map, Cat.FreeRefl.quotientFunctor_map_cons, Cat.freeMapIdIso_inv_app, Cat.freeMapCompIso_inv_app, Prefunctor.mapPath_comp'

SimpleGraph.Path

Definitions

NameCategoryTheorems
map πŸ“–CompOp
2 mathmath: map_coe, map_injective
mapEmbedding πŸ“–CompOp
2 mathmath: mapEmbedding_coe, mapEmbedding_injective
nil πŸ“–CompOp
2 mathmath: nil_coe, loop_eq
reverse πŸ“–CompOp
1 mathmath: reverse_coe
singleton πŸ“–CompOp
2 mathmath: singleton_coe, mk'_mem_edges_singleton

Theorems

NameKindAssumesProvesValidatesDepends On
cons_isCycle πŸ“–mathematicalSimpleGraph.Adj
Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.cons
β€”β€”
count_edges_eq_one πŸ“–mathematicalSym2
SimpleGraph.Walk.edges
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
Sym2.instDecidableEqβ€”List.count_eq_one_of_mem
SimpleGraph.Walk.IsTrail.edges_nodup
SimpleGraph.Walk.IsPath.isTrail
count_support_eq_one πŸ“–β€”SimpleGraph.Walk.support
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
β€”β€”List.count_eq_one_of_mem
SimpleGraph.Walk.IsPath.support_nodup
isPath πŸ“–mathematicalβ€”SimpleGraph.Walk.IsPath
SimpleGraph.Walk
β€”β€”
isTrail πŸ“–mathematicalβ€”SimpleGraph.Walk.IsTrail
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
β€”SimpleGraph.Walk.IsPath.isTrail
loop_eq πŸ“–mathematicalβ€”nilβ€”β€”
mapEmbedding_coe πŸ“–mathematicalβ€”SimpleGraph.Walk
DFunLike.coe
SimpleGraph.Embedding
RelEmbedding.instFunLike
SimpleGraph.Adj
SimpleGraph.Walk.IsPath
mapEmbedding
SimpleGraph.Walk.map
SimpleGraph.Embedding.toHom
β€”β€”
mapEmbedding_injective πŸ“–mathematicalβ€”SimpleGraph.Path
DFunLike.coe
SimpleGraph.Embedding
RelEmbedding.instFunLike
SimpleGraph.Adj
mapEmbedding
β€”map_injective
RelEmbedding.injective
map_coe πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
map
SimpleGraph.Walk.map
β€”β€”
map_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
SimpleGraph.Path
map
β€”SimpleGraph.Walk.map_injective_of_injective
mk'_mem_edges_singleton πŸ“–mathematicalSimpleGraph.AdjSym2
SimpleGraph.Walk.edges
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
singleton
β€”β€”
nil_coe πŸ“–mathematicalβ€”SimpleGraph.Walk
SimpleGraph.Walk.IsPath
nil
SimpleGraph.Walk.nil
β€”β€”
nodup_support πŸ“–mathematicalβ€”SimpleGraph.Walk.support
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
β€”SimpleGraph.Walk.isPath_def
notMem_edges_of_loop πŸ“–mathematicalβ€”Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk
SimpleGraph.Walk.IsPath
β€”loop_eq
reverse_coe πŸ“–mathematicalβ€”SimpleGraph.Walk
SimpleGraph.Walk.IsPath
reverse
SimpleGraph.Walk.reverse
β€”β€”
singleton_coe πŸ“–mathematicalSimpleGraph.AdjSimpleGraph.Walk
SimpleGraph.Walk.IsPath
singleton
SimpleGraph.Walk.cons
SimpleGraph.Walk.nil
β€”β€”

SimpleGraph.Walk

Definitions

NameCategoryTheorems
IsCircuit πŸ“–CompData
4 mathmath: IsCycle.toIsCircuit, isCircuit_def, IsCycle.isCircuit, isCircuit_copy
IsCycle πŸ“–CompData
20 mathmath: IsTrail.isCycle_cycleBypass, SimpleGraph.exists_girth_eq_length, IsHamiltonianCycle.isCycle, isCycle_def, SimpleGraph.exists_egirth_eq_length, cons_isCycle_iff, SimpleGraph.is3Clique_iff_exists_cycle_length_three, isHamiltonianCycle_isCycle_and_isHamiltonian_tail, map_isCycle_iff_of_injective, SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, isCycle_copy, isCycle_iff_isPath_tail_and_le_length, IsHamiltonianCycle.toIsCycle, IsCycle.not_of_nil, isHamiltonianCycle_iff_isCycle_and_length_eq, SimpleGraph.Path.cons_isCycle, mapLe_isCycle, SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp, isCycle_reverse, isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one
IsPath πŸ“–CompData
45 mathmath: SimpleGraph.Reachable.exists_isPath, SimpleGraph.isTree_iff_existsUnique_path, bypass_isPath, support_toPath_subset, SimpleGraph.Path.mapEmbedding_coe, SimpleGraph.IsAcyclic.isPath_iff_isChain, SimpleGraph.IsAcyclic.isPath_iff_isTrail, cons_isCycle_iff, SimpleGraph.Path.singleton_coe, isPath_def, mapLe_isPath, darts_toPath_subset, isPath_of_length_eq_dist, SimpleGraph.Connected.exists_isPath, IsHamiltonian.isPath, map_isPath_iff_of_injective, isCycle_iff_isPath_tail_and_le_length, SimpleGraph.Path.isPath, SimpleGraph.Path.reverse_coe, SimpleGraph.Path.notMem_edges_of_loop, isHamiltonian_iff_isPath_and_length_eq, isPath_reverse_iff, IsCycle.isPath_of_append_right, SimpleGraph.Connected.exists_path_of_dist, SimpleGraph.Path.nodup_support, SimpleGraph.Path.isTrail, IsPath.getVert_injOn_iff, isPath_copy, SimpleGraph.Path.nil_coe, IsPath.nil, SimpleGraph.Path.mk'_mem_edges_singleton, SimpleGraph.IsTree.existsUnique_path, IsCycle.isPath_of_append_left, edges_toPath_subset, SimpleGraph.Path.map_coe, SimpleGraph.Preconnected.exists_isPath, cons_isPath_iff, isPath_iff_injective_get_support, IsPath.mk', isPath_iff_eq_nil, SimpleGraph.Reachable.exists_path_of_dist, IsPath.of_adj, IsCycle.isPath_takeUntil, concat_isPath_iff, IsCycle.isPath_tail
IsTrail πŸ“–CompData
18 mathmath: isEulerian_iff, IsPath.isTrail, isCycle_def, SimpleGraph.IsAcyclic.isPath_iff_isTrail, isTrail_def, IsEulerian.isTrail, isCircuit_def, IsCircuit.isTrail, IsTrail.nil, SimpleGraph.Path.isTrail, isTrail_copy, IsPath.toIsTrail, map_isTrail_iff_of_injective, cons_isTrail_iff, mapLe_isTrail, reverse_isTrail_iff, isTrail_cons, IsCircuit.toIsTrail
bypass πŸ“–CompOp
7 mathmath: bypass_isPath, length_bypass_le, bypass_copy, toSubgraph_bypass_le_toSubgraph, edges_bypass_subset, darts_bypass_subset, support_bypass_subset
cycleBypass πŸ“–CompOp
3 mathmath: IsTrail.isCycle_cycleBypass, edges_cycleBypass_subset, cycleBypass_nil
instDecidableIsPathOfDecidableEq πŸ“–CompOpβ€”
toPath πŸ“–CompOp
3 mathmath: support_toPath_subset, darts_toPath_subset, edges_toPath_subset

Theorems

NameKindAssumesProvesValidatesDepends On
bypass_copy πŸ“–mathematicalβ€”bypass
copy
β€”β€”
bypass_eq_self_of_length_le πŸ“–β€”length
bypass
β€”β€”length_dropUntil_le
length_bypass_le
bypass_isPath πŸ“–mathematicalβ€”IsPath
bypass
β€”IsPath.dropUntil
concat_isPath_iff πŸ“–mathematicalSimpleGraph.AdjIsPath
concat
support
β€”isPath_reverse_iff
SimpleGraph.symm
reverse_concat
support_reverse
cons_isPath_iff
SimpleGraph.Adj.symm
cons_isCycle_iff πŸ“–mathematicalSimpleGraph.AdjIsCycle
cons
IsPath
Sym2
edges
β€”edges_nodup_of_support_nodup
cons_isPath_iff πŸ“–mathematicalSimpleGraph.AdjIsPath
cons
support
β€”β€”
cons_isTrail_iff πŸ“–mathematicalSimpleGraph.AdjIsTrail
cons
Sym2
edges
β€”isTrail_cons
cycleBypass_nil πŸ“–mathematicalβ€”cycleBypass
nil
β€”β€”
darts_bypass_subset πŸ“–mathematicalβ€”SimpleGraph.Dart
darts
bypass
β€”darts_dropUntil_subset
darts_cons
darts_toPath_subset πŸ“–mathematicalβ€”SimpleGraph.Dart
darts
SimpleGraph.Walk
IsPath
toPath
β€”darts_bypass_subset
edges_bypass_subset πŸ“–mathematicalβ€”Sym2
edges
bypass
β€”darts_bypass_subset
edges_cycleBypass_subset πŸ“–mathematicalβ€”Sym2
edges
cycleBypass
β€”edges_bypass_subset
edges_toPath_subset πŸ“–mathematicalβ€”Sym2
edges
SimpleGraph.Walk
IsPath
toPath
β€”edges_bypass_subset
endpoint_notMem_support_takeUntil πŸ“–mathematicalIsPath
support
takeUntilβ€”mem_support_iff_exists_getVert
length_takeUntil_lt
IsPath.getVert_injOn
Set.mem_setOf
getVert_length
getVert_takeUntil
exists_isPath_forall_isPath_length_le_length πŸ“–mathematicalβ€”lengthβ€”Set.Finite.subset
Set.finite_le_nat
IsTrail.length_le_card_edgeFinset
IsPath.isTrail
Set.Finite.exists_maximal
instIsTransLe
exists_isTrail_forall_isTrail_length_le_length πŸ“–mathematicalβ€”lengthβ€”Set.Finite.subset
Set.finite_le_nat
IsTrail.length_le_card_edgeFinset
Set.Finite.exists_maximal
instIsTransLe
isCircuit_copy πŸ“–mathematicalβ€”IsCircuit
copy
β€”β€”
isCircuit_def πŸ“–mathematicalβ€”IsCircuit
IsTrail
β€”β€”
isCycle_copy πŸ“–mathematicalβ€”IsCycle
copy
β€”β€”
isCycle_def πŸ“–mathematicalβ€”IsCycle
IsTrail
support
β€”IsCircuit.isTrail
IsCycle.isCircuit
IsCircuit.ne_nil
IsCycle.support_nodup
isCycle_iff_isPath_tail_and_le_length πŸ“–mathematicalβ€”IsCycle
IsPath
snd
tail
length
β€”IsCycle.isPath_tail
IsCycle.three_le_length
cons_isCycle_iff
getVert_zero
tail_cons
length_support
head_support
IsPath.eq_penultimate_of_mem_edges
support_getElem_length_sub_one_eq_penultimate
isPath_iff_injective_get_support
isCycle_reverse πŸ“–mathematicalβ€”IsCycle
reverse
β€”reverse_reverse
IsCycle.reverse
isPath_copy πŸ“–mathematicalβ€”IsPath
copy
β€”β€”
isPath_def πŸ“–mathematicalβ€”IsPath
support
β€”IsPath.support_nodup
IsPath.mk'
isPath_iff_eq_nil πŸ“–mathematicalβ€”IsPath
nil
β€”β€”
isPath_iff_injective_get_support πŸ“–mathematicalβ€”IsPath
support
β€”isPath_def
List.nodup_iff_injective_get
isPath_of_isSubwalk πŸ“–β€”IsSubwalk
IsPath
β€”β€”IsPath.of_append_right
IsPath.of_append_left
isPath_reverse_iff πŸ“–mathematicalβ€”IsPath
reverse
β€”reverse_reverse
IsPath.reverse
isTrail_cons πŸ“–mathematicalSimpleGraph.AdjIsTrail
cons
Sym2
edges
β€”β€”
isTrail_copy πŸ“–mathematicalβ€”IsTrail
copy
β€”β€”
isTrail_def πŸ“–mathematicalβ€”IsTrail
Sym2
edges
β€”β€”
isTrail_of_isSubwalk πŸ“–β€”IsSubwalk
IsTrail
β€”β€”IsTrail.of_append_right
IsTrail.of_append_left
length_bypass_le πŸ“–mathematicalβ€”length
bypass
β€”le_refl
length_dropUntil_le
length_cons
mapLe_isCycle πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
IsCycle
mapLe
β€”map_isCycle_iff_of_injective
mapLe_isPath πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
IsPath
mapLe
β€”map_isPath_iff_of_injective
mapLe_isTrail πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
IsTrail
mapLe
β€”map_isTrail_iff_of_injective
map_isCycle_iff_of_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
IsCycle
map
β€”isCycle_def
map_isTrail_iff_of_injective
map_eq_nil_iff
support_map
List.nodup_map_iff
map_isPath_iff_of_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
IsPath
map
β€”IsPath.of_map
map_isPath_of_injective
map_isPath_of_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
IsPath
mapβ€”SimpleGraph.Hom.map_adj
cons_isPath_iff
support_map
map_isTrail_iff_of_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
IsTrail
map
β€”SimpleGraph.Hom.map_adj
map_cons
isTrail_cons
edges_map
List.mem_map_of_injective
Sym2.map.injective
map_isTrail_of_injective πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
IsTrail
mapβ€”map_isTrail_iff_of_injective
not_nil_of_isCycle_cons πŸ“–mathematicalSimpleGraph.Adj
IsCycle
cons
Nilβ€”IsCycle.three_le_length
length_cons
not_nil_iff_lt_length
reverse_isTrail_iff πŸ“–mathematicalβ€”IsTrail
reverse
β€”reverse_reverse
IsTrail.reverse
support_bypass_subset πŸ“–mathematicalβ€”support
bypass
β€”support_dropUntil_subset
support_cons
support_toPath_subset πŸ“–mathematicalβ€”support
SimpleGraph.Walk
IsPath
toPath
β€”support_bypass_subset
toDeleteEdges_copy πŸ“–mathematicalSym2
Set
Set.instMembership
toDeleteEdges
copy
SimpleGraph.deleteEdges
β€”β€”

SimpleGraph.Walk.IsCircuit

Theorems

NameKindAssumesProvesValidatesDepends On
isTrail πŸ“–mathematicalSimpleGraph.Walk.IsCircuitSimpleGraph.Walk.IsTrailβ€”β€”
ne_nil πŸ“–β€”SimpleGraph.Walk.IsCircuitβ€”β€”β€”
not_nil πŸ“–mathematicalSimpleGraph.Walk.IsCircuitSimpleGraph.Walk.Nilβ€”ne_nil
SimpleGraph.Walk.Nil.eq_nil
rotate πŸ“–mathematicalSimpleGraph.Walk.IsCircuit
SimpleGraph.Walk.support
SimpleGraph.Walk.rotateβ€”SimpleGraph.Walk.IsTrail.rotate
isTrail
ne_nil
SimpleGraph.Walk.take_spec
SimpleGraph.Walk.length_append
add_comm
SimpleGraph.Walk.rotate.eq_1
toIsTrail πŸ“–mathematicalSimpleGraph.Walk.IsCircuitSimpleGraph.Walk.IsTrailβ€”isTrail

SimpleGraph.Walk.IsCycle

Theorems

NameKindAssumesProvesValidatesDepends On
count_support πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.supportβ€”List.count_eq_one_of_mem
support_nodup
SimpleGraph.Walk.end_mem_tail_support
not_nil
SimpleGraph.Walk.support_ne_nil
SimpleGraph.Walk.head_support
count_support_of_mem πŸ“–β€”SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.support
β€”β€”SimpleGraph.Walk.support_ne_nil
List.count_eq_one_of_mem
support_nodup
SimpleGraph.Walk.head_support
getVert_endpoint_iff πŸ“–mathematicalSimpleGraph.Walk.IsCycle
SimpleGraph.Walk.length
SimpleGraph.Walk.getVertβ€”getVert_injOn
SimpleGraph.Walk.getVert_length
SimpleGraph.Walk.getVert_zero
getVert_injOn πŸ“–mathematicalSimpleGraph.Walk.IsCycleSet.InjOn
SimpleGraph.Walk.getVert
setOf
SimpleGraph.Walk.length
β€”SimpleGraph.Walk.IsPath.getVert_injOn
SimpleGraph.Walk.adj_snd
not_nil
SimpleGraph.Walk.cons_isCycle_iff
SimpleGraph.Walk.cons_tail_eq
Set.mem_setOf
SimpleGraph.Walk.length_tail_add_one
SimpleGraph.Walk.not_nil_of_tail_not_nil
SimpleGraph.Walk.not_nil_of_isCycle_cons
SimpleGraph.Walk.getVert_tail
getVert_injOn' πŸ“–mathematicalSimpleGraph.Walk.IsCycleSet.InjOn
SimpleGraph.Walk.getVert
setOf
SimpleGraph.Walk.length
β€”three_le_length
getVert_injOn
reverse
SimpleGraph.Walk.length_reverse
SimpleGraph.Walk.getVert_reverse
getVert_sub_one_ne_getVert_add_one πŸ“–β€”SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.length
β€”β€”three_le_length
getVert_endpoint_iff
SimpleGraph.Walk.getVert_of_length_le
getVert_injOn'
isCircuit πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.IsCircuitβ€”β€”
isPath_of_append_left πŸ“–mathematicalSimpleGraph.Walk.Nil
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.append
SimpleGraph.Walk.IsPathβ€”SimpleGraph.Walk.isPath_reverse_iff
isPath_of_append_right
reverse
SimpleGraph.Walk.reverse_append
isPath_of_append_right πŸ“–mathematicalSimpleGraph.Walk.Nil
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.append
SimpleGraph.Walk.IsPathβ€”support_nodup
SimpleGraph.Walk.isPath_def
SimpleGraph.Walk.support_eq_cons
List.nodup_append'
SimpleGraph.Walk.tail_support_append
SimpleGraph.Walk.end_mem_tail_support
isPath_tail πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.IsPath
SimpleGraph.Walk.snd
SimpleGraph.Walk.tail
β€”SimpleGraph.Walk.IsPath.mk'
support_nodup
SimpleGraph.Walk.support_tail_of_not_nil
not_nil
isPath_takeUntil πŸ“–mathematicalSimpleGraph.Walk.IsCycle
SimpleGraph.Walk.support
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.takeUntil
β€”SimpleGraph.Walk.takeUntil_first
SimpleGraph.Walk.isPath_reverse_iff
isPath_of_append_right
SimpleGraph.Walk.not_nil_of_ne
SimpleGraph.Walk.reverse_append
SimpleGraph.Walk.take_spec
SimpleGraph.Walk.isCycle_reverse
map πŸ“–mathematicalDFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.mapβ€”SimpleGraph.Walk.map_isCycle_iff_of_injective
mapLe πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.mapLeβ€”SimpleGraph.Walk.mapLe_isCycle
ne_bot πŸ“–β€”SimpleGraph.Walk.IsCycleβ€”β€”SimpleGraph.Walk.IsCircuit.ne_nil
isCircuit
not_nil πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.Nilβ€”SimpleGraph.Walk.IsCircuit.ne_nil
isCircuit
SimpleGraph.Walk.Nil.eq_nil
not_of_nil πŸ“–mathematicalβ€”SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.nil
β€”SimpleGraph.Walk.IsCircuit.ne_nil
isCircuit
of_mapLe πŸ“–β€”SimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsCycle
SimpleGraph.Walk.mapLe
β€”β€”SimpleGraph.Walk.mapLe_isCycle
reverse πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.reverseβ€”SimpleGraph.Walk.IsTrail.reverse
SimpleGraph.Walk.length_reverse
rotate πŸ“–mathematicalSimpleGraph.Walk.IsCycle
SimpleGraph.Walk.support
SimpleGraph.Walk.rotateβ€”SimpleGraph.Walk.IsCircuit.rotate
isCircuit
List.IsRotated.nodup_iff
SimpleGraph.Walk.support_rotate
support_nodup
snd_ne_penultimate πŸ“–β€”SimpleGraph.Walk.IsCycleβ€”β€”three_le_length
getVert_injOn
support_nodup πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.supportβ€”β€”
three_le_length πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.lengthβ€”β€”
toDeleteEdges πŸ“–mathematicalSimpleGraph.Walk.IsCycle
Sym2
Set
Set.instMembership
SimpleGraph.deleteEdges
SimpleGraph.Walk.toDeleteEdges
β€”transfer
toIsCircuit πŸ“–mathematicalSimpleGraph.Walk.IsCycleSimpleGraph.Walk.IsCircuitβ€”isCircuit
transfer πŸ“–mathematicalSimpleGraph.Walk.IsCycle
Sym2
Set
Set.instMembership
SimpleGraph.edgeSet
SimpleGraph.Walk.transferβ€”SimpleGraph.Walk.edges_transfer
SimpleGraph.Walk.IsPath.transfer

SimpleGraph.Walk.IsPath

Theorems

NameKindAssumesProvesValidatesDepends On
concat πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.support
SimpleGraph.Adj
SimpleGraph.Walk.concatβ€”SimpleGraph.Walk.concat_isPath_iff
cons πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.support
SimpleGraph.Adj
SimpleGraph.Walk.consβ€”SimpleGraph.Walk.cons_isPath_iff
disjoint_support_of_append πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.append
SimpleGraph.Walk.Nil
SimpleGraph.Walk.support
SimpleGraph.Walk.snd
SimpleGraph.Walk.tail
β€”support_nodup
SimpleGraph.Walk.support_tail_of_not_nil
List.disjoint_of_nodup_append
SimpleGraph.Walk.support_append
dropUntil πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.support
SimpleGraph.Walk.dropUntilβ€”of_append_right
SimpleGraph.Walk.take_spec
eq_penultimate_of_mem_edges πŸ“–mathematicalSimpleGraph.Walk.IsPath
Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk.penultimateβ€”SimpleGraph.Walk.edges_reverse
SimpleGraph.Walk.snd_reverse
eq_snd_of_mem_edges
SimpleGraph.Walk.isPath_reverse_iff
eq_snd_of_mem_edges πŸ“–mathematicalSimpleGraph.Walk.IsPath
Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk.sndβ€”Iff.not
SimpleGraph.Walk.edges_eq_nil
SimpleGraph.Walk.getVert_zero
SimpleGraph.Walk.tail_cons
SimpleGraph.Walk.support_copy
Sym2.rel_iff'
Sym2.eq
SimpleGraph.Walk.adj_snd
SimpleGraph.Walk.edges_cons
SimpleGraph.Walk.cons_tail_eq
getVert_eq_end_iff πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.length
SimpleGraph.Walk.getVertβ€”getVert_eq_start_iff
reverse
SimpleGraph.Walk.length_reverse
SimpleGraph.Walk.getVert_reverse
getVert_eq_start_iff πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.length
SimpleGraph.Walk.getVertβ€”getVert_injOn
Set.mem_setOf
SimpleGraph.Walk.getVert_zero
getVert_injOn πŸ“–mathematicalSimpleGraph.Walk.IsPathSet.InjOn
SimpleGraph.Walk.getVert
setOf
SimpleGraph.Walk.length
β€”SimpleGraph.Walk.getVert_zero
SimpleGraph.Walk.getVert_cons
SimpleGraph.Walk.mem_support_iff_exists_getVert
of_cons
getVert_injOn_iff πŸ“–mathematicalβ€”Set.InjOn
SimpleGraph.Walk.getVert
setOf
SimpleGraph.Walk.length
SimpleGraph.Walk.IsPath
β€”SimpleGraph.Walk.cons_isPath_iff
SimpleGraph.Walk.length_cons
SimpleGraph.Walk.mem_support_iff_exists_getVert
SimpleGraph.Walk.getVert_cons
SimpleGraph.Walk.getVert_zero
getVert_injOn
isTrail πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.IsTrailβ€”β€”
length_lt πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.length
Fintype.card
β€”SimpleGraph.Walk.length_support
List.Nodup.length_le_card
support_nodup
mapLe πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.mapLeβ€”SimpleGraph.Walk.mapLe_isPath
mem_support_iff_exists_append πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.support
SimpleGraph.Walk.append
β€”SimpleGraph.Walk.mem_support_iff_exists_append
of_append_left
of_append_right
mk' πŸ“–mathematicalSimpleGraph.Walk.supportSimpleGraph.Walk.IsPathβ€”SimpleGraph.Walk.edges_nodup_of_support_nodup
ne_of_mem_support_of_append πŸ“–β€”SimpleGraph.Walk.IsPath
SimpleGraph.Walk.append
SimpleGraph.Walk.support
β€”β€”SimpleGraph.Walk.nil_iff_support_eq
SimpleGraph.Walk.support_tail_of_not_nil
SimpleGraph.Walk.mem_support_iff
disjoint_support_of_append
nil πŸ“–mathematicalβ€”SimpleGraph.Walk.IsPath
SimpleGraph.Walk.nil
β€”β€”
of_adj πŸ“–mathematicalSimpleGraph.AdjSimpleGraph.Walk.IsPath
SimpleGraph.Adj.toWalk
β€”β€”
of_append_left πŸ“–β€”SimpleGraph.Walk.IsPath
SimpleGraph.Walk.append
β€”β€”SimpleGraph.Walk.support_append
List.Nodup.of_append_left
of_append_right πŸ“–β€”SimpleGraph.Walk.IsPath
SimpleGraph.Walk.append
β€”β€”SimpleGraph.Walk.isPath_reverse_iff
of_append_left
SimpleGraph.Walk.reverse_append
of_cons πŸ“–β€”SimpleGraph.Adj
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.cons
β€”β€”β€”
of_map πŸ“–β€”SimpleGraph.Walk.IsPath
DFunLike.coe
SimpleGraph.Hom
RelHom.instFunLike
SimpleGraph.Adj
SimpleGraph.Walk.map
β€”β€”β€”
of_mapLe πŸ“–β€”SimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.mapLe
β€”β€”SimpleGraph.Walk.mapLe_isPath
reverse πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.reverseβ€”SimpleGraph.Walk.support_reverse
support_nodup πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.supportβ€”β€”
tail πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.snd
SimpleGraph.Walk.tail
β€”SimpleGraph.Walk.getVert_zero
SimpleGraph.Walk.tail_cons
SimpleGraph.Walk.support_copy
takeUntil πŸ“–mathematicalSimpleGraph.Walk.IsPath
SimpleGraph.Walk.support
SimpleGraph.Walk.takeUntilβ€”of_append_left
SimpleGraph.Walk.take_spec
toDeleteEdges πŸ“–mathematicalSimpleGraph.Walk.IsPath
Sym2
Set
Set.instMembership
SimpleGraph.deleteEdges
SimpleGraph.Walk.toDeleteEdges
β€”transfer
toIsTrail πŸ“–mathematicalSimpleGraph.Walk.IsPathSimpleGraph.Walk.IsTrailβ€”isTrail
transfer πŸ“–mathematicalSym2
Set
Set.instMembership
SimpleGraph.edgeSet
SimpleGraph.Walk.IsPath
SimpleGraph.Walk.transferβ€”SimpleGraph.Walk.support_transfer

SimpleGraph.Walk.IsTrail

Theorems

NameKindAssumesProvesValidatesDepends On
cons πŸ“–mathematicalSimpleGraph.Walk.IsTrail
SimpleGraph.Adj
Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk.consβ€”β€”
count_edges_eq_one πŸ“–mathematicalSimpleGraph.Walk.IsTrail
Sym2
SimpleGraph.Walk.edges
Sym2.instDecidableEqβ€”List.count_eq_one_of_mem
edges_nodup
count_edges_le_one πŸ“–mathematicalSimpleGraph.Walk.IsTrailSym2
Sym2.instDecidableEq
SimpleGraph.Walk.edges
β€”List.nodup_iff_count_le_one
edges_nodup
disjoint_edges_takeUntil_dropUntil πŸ“–mathematicalSimpleGraph.Walk.IsTrail
SimpleGraph.Walk.support
Sym2
SimpleGraph.Walk.edges
SimpleGraph.Walk.takeUntil
SimpleGraph.Walk.dropUntil
β€”List.disjoint_of_nodup_append
SimpleGraph.Walk.take_spec
edges_nodup
dropUntil πŸ“–mathematicalSimpleGraph.Walk.IsTrail
SimpleGraph.Walk.support
SimpleGraph.Walk.dropUntilβ€”of_append_right
SimpleGraph.Walk.take_spec
edges_nodup πŸ“–mathematicalSimpleGraph.Walk.IsTrailSym2
SimpleGraph.Walk.edges
β€”β€”
isCycle_cycleBypass πŸ“–mathematicalSimpleGraph.Walk.IsTrailSimpleGraph.Walk.IsCycle
SimpleGraph.Walk.cycleBypass
β€”cons
SimpleGraph.Walk.IsPath.isTrail
SimpleGraph.Walk.bypass_isPath
SimpleGraph.Walk.edges_bypass_subset
SimpleGraph.Walk.IsPath.support_nodup
length_le_card_edgeFinset πŸ“–mathematicalSimpleGraph.Walk.IsTrailSimpleGraph.Walk.length
Finset.card
Sym2
SimpleGraph.edgeFinset
β€”List.toFinset_card_of_nodup
edges_nodup
SimpleGraph.Walk.length_edges
SimpleGraph.mem_edgeFinset
SimpleGraph.Walk.edges_subset_edgeSet
Finset.card_le_card
mapLe πŸ“–mathematicalSimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.mapLeβ€”SimpleGraph.Walk.mapLe_isTrail
nil πŸ“–mathematicalβ€”SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.nil
β€”β€”
of_append_left πŸ“–β€”SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.append
β€”β€”SimpleGraph.Walk.edges_append
SimpleGraph.Walk.isTrail_def
of_append_right πŸ“–β€”SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.append
β€”β€”SimpleGraph.Walk.edges_append
SimpleGraph.Walk.isTrail_def
of_cons πŸ“–β€”SimpleGraph.Adj
SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.cons
β€”β€”β€”
of_mapLe πŸ“–β€”SimpleGraph
SimpleGraph.instLE
SimpleGraph.Walk.IsTrail
SimpleGraph.Walk.mapLe
β€”β€”SimpleGraph.Walk.mapLe_isTrail
reverse πŸ“–mathematicalSimpleGraph.Walk.IsTrailSimpleGraph.Walk.reverseβ€”SimpleGraph.Walk.edges_reverse
rotate πŸ“–mathematicalSimpleGraph.Walk.IsTrail
SimpleGraph.Walk.support
SimpleGraph.Walk.rotateβ€”SimpleGraph.Walk.isTrail_def
List.IsRotated.perm
SimpleGraph.Walk.rotate_edges
edges_nodup
takeUntil πŸ“–mathematicalSimpleGraph.Walk.IsTrail
SimpleGraph.Walk.support
SimpleGraph.Walk.takeUntilβ€”of_append_left
SimpleGraph.Walk.take_spec

---

← Back to Index