Subgraph

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

Statistics

Metric	Count
Definitions toSubgraph, Preconnected, instCoeConnectedConnectedElemVertsCoe, instCoeFunConnectedForallForallReachableElemVertsCoe, instCoeFunPreconnectedForallForallReachableElemVertsCoe, instCoePreconnectedPreconnectedElemVertsCoe, mapToSubgraph, toSubgraph	8
Theorems toSubgraph, coe_toSubgraph, connected_toSubgraph, maximal_connected_toSubgraph, maximal_subgraph_connected_iff, spanningCoe_toSubgraph, toSubgraph, coe_coeSubgraph, coe_subgraphMap, coe_toSubgraph, adj_union, coeSubgraph, exists_verts_eq_connectedComponentSupp, induce_verts, map, mono, mono', nonempty, preconnected, sup, coeSubgraph, degree_zero_iff, exists_adj_of_nontrivial, map, connected_iff, connected_iff', connected_iff_forall_exists_walk_subgraph, connected_induce_top_sup, connected_sup, induce_union_connected, preconnected_iff, preconnected_iff_forall_exists_walk_subgraph, singletonSubgraph_connected, subgraphOfAdj_connected, top_induce_pair_connected_of_adj, exists_isCycle_snd_verts_eq, ncard_neighborSet_toSubgraph_eq_two, neighborSet_toSubgraph_endpoint, neighborSet_toSubgraph_internal, ncard_neighborSet_toSubgraph_internal_eq_two, neighborSet_toSubgraph_endpoint, neighborSet_toSubgraph_internal, neighborSet_toSubgraph_startpoint, snd_of_toSubgraph_adj, adj_toSubgraph_iff_mem_edges, adj_toSubgraph_mapLe, connected_induce_support, edgeSet_toSubgraph, end_mem_verts_toSubgraph, exists_mem_support_forall_mem_support_imp_eq, exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty, finite_neighborSet_toSubgraph, map_mapToSubgraph_eq_induce, map_mapToSubgraph_eq_induce_id, map_mapToSubgraph_hom, mem_edges_toSubgraph, mem_support_of_adj_toSubgraph, mem_verts_toSubgraph, not_nil_of_adj_toSubgraph, start_mem_verts_toSubgraph, toSubgraph_adj_getVert, toSubgraph_adj_iff, toSubgraph_adj_penultimate, toSubgraph_adj_snd, toSubgraph_append, toSubgraph_bypass_le_toSubgraph, toSubgraph_connected, toSubgraph_cons_nil_eq_subgraphOfAdj, toSubgraph_le_iff, toSubgraph_le_induce_support, toSubgraph_map, toSubgraph_reverse, toSubgraph_rotate, verts_toSubgraph, connected_induce_iff, connected_induce_union, extend_finset_to_connected, induce_connected_adj_union, induce_connected_of_patches, induce_pair_connected_of_adj, induce_sUnion_connected_of_pairwise_not_disjoint, induce_union_connected, preconnected_induce_iff	83
Total	91

SimpleGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connected_induce_iff 📖	mathematical	—	Connected Set.Elem induce Subgraph.Connected Subgraph.induce Top.top Subgraph Subgraph.instTop	—	induce_eq_coe_induce_top Subgraph.connected_iff'
connected_induce_union 📖	mathematical	Preconnected Set.Elem induce Set Set.instMembership Adj	Connected Set.instUnion	—	connected_induce_iff Subgraph.Connected.mono Subgraph.connected_induce_top_sup preconnected_induce_iff Subgraph.subgraphOfAdj_eq_induce subgraphOfAdj_le_of_adj Set.union_assoc
extend_finset_to_connected 📖	mathematical	Preconnected Finset.Nonempty	Finset Finset.instHasSubset Connected Set.Elem SetLike.coe Finset.instSetLike induce	—	Walk.end_mem_support induce_connected_of_patches Finset.coe_biUnion Set.iUnion_congr_Prop List.coe_toFinset Set.mem_iUnion₂ Connected.preconnected Walk.connected_induce_support
induce_connected_adj_union 📖	mathematical	Connected Set.Elem induce Set Set.instMembership Adj	Set.instUnion	—	connected_induce_union Connected.preconnected
induce_connected_of_patches 📖	mathematical	Set Set.instMembership Set.instHasSubset Reachable Set.Elem induce	Connected	—	connected_iff_exists_forall_reachable Reachable.map
induce_pair_connected_of_adj 📖	mathematical	Adj	Connected Set.Elem Set Set.instInsert Set.instSingletonSet induce	—	connected_induce_iff Subgraph.top_induce_pair_connected_of_adj
induce_sUnion_connected_of_pairwise_not_disjoint 📖	mathematical	Set.Nonempty Set Set.instInter Connected Set.Elem induce	Set.sUnion	—	Connected.nonempty induce_connected_of_patches Set.subset_sUnion_of_mem Set.union_subset Connected.preconnected induce_union_connected
induce_union_connected 📖	mathematical	Preconnected Set.Elem induce Set.Nonempty Set Set.instInter	Connected Set.instUnion	—	connected_induce_iff Subgraph.induce_union_connected preconnected_induce_iff
preconnected_induce_iff 📖	mathematical	—	Preconnected Set.Elem induce Subgraph.Preconnected Subgraph.induce Top.top Subgraph Subgraph.instTop	—	induce_eq_coe_induce_top Subgraph.preconnected_iff

SimpleGraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSubgraph 📖	mathematical	SimpleGraph SimpleGraph.instLE SimpleGraph.Connected	SimpleGraph.Subgraph.Connected SimpleGraph.toSubgraph	—	SimpleGraph.Subgraph.connected_iff SimpleGraph.Preconnected.toSubgraph preconnected nonempty

SimpleGraph.ConnectedComponent

Definitions

Name	Category	Theorems
toSubgraph 📖	CompOp	5 math math: coe_toSubgraph, maximal_connected_toSubgraph, spanningCoe_toSubgraph, maximal_subgraph_connected_iff, connected_toSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph.coe toSubgraph toSimpleGraph	—	SimpleGraph.induce_eq_coe_induce_top
connected_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph.Connected toSubgraph	—	connected_toSimpleGraph coe_toSubgraph
maximal_connected_toSubgraph 📖	mathematical	—	Maximal SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder SimpleGraph.Subgraph.Connected toSubgraph	—	ind connected_toSubgraph le_trans SimpleGraph.Subgraph.le_induce_top_verts SimpleGraph.Subgraph.induce_mono_right sound SimpleGraph.Reachable.map SimpleGraph.Connected.preconnected SimpleGraph.Subgraph.Connected.coe
maximal_subgraph_connected_iff 📖	mathematical	—	Maximal SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder SimpleGraph.Subgraph.Connected toSubgraph	—	SimpleGraph.Subgraph.Connected.nonempty le_trans SimpleGraph.Subgraph.le_induce_top_verts SimpleGraph.Subgraph.induce_mono_right sound SimpleGraph.Reachable.map SimpleGraph.Connected.preconnected SimpleGraph.Subgraph.Connected.coe le_antisymm connected_toSubgraph maximal_connected_toSubgraph
spanningCoe_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph.spanningCoe toSubgraph SimpleGraph.spanningCoe SetLike.coe SimpleGraph.ConnectedComponent instSetLike toSimpleGraph	—	SimpleGraph.spanningCoe_induce_top

SimpleGraph.Preconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSubgraph 📖	mathematical	SimpleGraph SimpleGraph.instLE SimpleGraph.Preconnected	SimpleGraph.Subgraph.Preconnected SimpleGraph.toSubgraph	—	SimpleGraph.Subgraph.preconnected_iff SimpleGraph.Reachable.coe_toSubgraph

SimpleGraph.Reachable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_coeSubgraph 📖	mathematical	—	SimpleGraph.Reachable Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coeSubgraph SimpleGraph.Subgraph.coe SimpleGraph.Subgraph.vert Set Set.instMembership	—	coe_subgraphMap
coe_subgraphMap 📖	mathematical	—	SimpleGraph.Reachable Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.map SimpleGraph.Subgraph.coe Set Set.instMembership DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj Set.mem_image_of_mem Subtype.prop	—	map Set.mem_image_of_mem Subtype.prop Relation.map_apply
coe_toSubgraph 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.Reachable Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.toSubgraph SimpleGraph.Subgraph.coe Set Set.instMembership	—	map

SimpleGraph.Subgraph

Definitions

Name	Category	Theorems
Preconnected 📖	CompData	6 math math: Connected.preconnected, preconnected_iff, SimpleGraph.Preconnected.toSubgraph, SimpleGraph.preconnected_induce_iff, preconnected_iff_forall_exists_walk_subgraph, connected_iff
instCoeConnectedConnectedElemVertsCoe 📖	CompOp	—
instCoeFunConnectedForallForallReachableElemVertsCoe 📖	CompOp	—
instCoeFunPreconnectedForallForallReachableElemVertsCoe 📖	CompOp	—
instCoePreconnectedPreconnectedElemVertsCoe 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connected_iff 📖	mathematical	—	Connected Preconnected Set.Nonempty verts	—	connected_iff' SimpleGraph.connected_iff preconnected_iff Set.nonempty_coe_sort
connected_iff' 📖	mathematical	—	Connected SimpleGraph.Connected Set.Elem verts coe	—	—
connected_iff_forall_exists_walk_subgraph 📖	mathematical	—	Connected Set.Nonempty verts SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder instPartialOrder SimpleGraph.Walk.toSubgraph	—	connected_iff preconnected_iff_forall_exists_walk_subgraph
connected_induce_top_sup 📖	mathematical	Preconnected Set Set.instMembership verts SimpleGraph.Adj	Connected SimpleGraph.Subgraph instMax induce Top.top instTop Set.instInsert Set.instSingletonSet	—	connected_sup Connected.preconnected top_induce_pair_connected_of_adj
connected_sup 📖	mathematical	Preconnected Set.Nonempty verts SimpleGraph.Subgraph instMin	Connected instMax	—	connected_iff' SimpleGraph.connected_iff_exists_forall_reachable SimpleGraph.Reachable.map le_sup_left Preconnected.coe le_sup_right
induce_union_connected 📖	mathematical	Preconnected induce Set.Nonempty Set SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Connected Set.instUnion	—	Connected.mono le_induce_union connected_sup
preconnected_iff 📖	mathematical	—	Preconnected SimpleGraph.Preconnected Set.Elem verts coe	—	—
preconnected_iff_forall_exists_walk_subgraph 📖	mathematical	—	Preconnected SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder instPartialOrder SimpleGraph.Walk.toSubgraph	—	SimpleGraph.Reachable.elim Preconnected.coe SimpleGraph.Walk.toSubgraph_map preconnected_iff SimpleGraph.Reachable.map SimpleGraph.Walk.start_mem_verts_toSubgraph SimpleGraph.Walk.end_mem_verts_toSubgraph SimpleGraph.Walk.toSubgraph_connected
singletonSubgraph_connected 📖	mathematical	—	Connected SimpleGraph.singletonSubgraph	—	SimpleGraph.Reachable.refl SimpleGraph.nonempty_singletonSubgraph_verts
subgraphOfAdj_connected 📖	mathematical	SimpleGraph.Adj	Connected SimpleGraph.subgraphOfAdj	—	SimpleGraph.Reachable.refl SimpleGraph.Adj.reachable SimpleGraph.nonempty_subgraphOfAdj_verts
top_induce_pair_connected_of_adj 📖	mathematical	SimpleGraph.Adj	Connected induce Top.top SimpleGraph.Subgraph instTop Set Set.instInsert Set.instSingletonSet	—	subgraphOfAdj_eq_induce subgraphOfAdj_connected

SimpleGraph.Subgraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_union 📖	mathematical	SimpleGraph.Subgraph.Connected Set Set.instMembership SimpleGraph.Subgraph.verts SimpleGraph.Adj	SimpleGraph.Subgraph SimpleGraph.Subgraph.instMax SimpleGraph.Subgraph.induce Top.top SimpleGraph.Subgraph.instTop Set.instInsert Set.instSingletonSet	—	SimpleGraph.Subgraph.connected_induce_top_sup preconnected
coeSubgraph 📖	mathematical	SimpleGraph.Subgraph.Connected Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	SimpleGraph.Subgraph.coeSubgraph	—	map
exists_verts_eq_connectedComponentSupp 📖	mathematical	SimpleGraph.Subgraph.Connected SimpleGraph.Subgraph.Adj	SimpleGraph.Subgraph.verts SimpleGraph.ConnectedComponent.supp	—	SimpleGraph.ConnectedComponent.exists nonempty Set.ext SimpleGraph.Reachable.map SimpleGraph.Reachable.mem_subgraphVerts SimpleGraph.Reachable.symm
induce_verts 📖	mathematical	SimpleGraph.Subgraph.Connected	SimpleGraph.Connected Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.induce	—	SimpleGraph.connected_induce_iff mono SimpleGraph.Subgraph.le_induce_top_verts
map 📖	mathematical	SimpleGraph.Subgraph.Connected Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	SimpleGraph.Subgraph.map	—	SimpleGraph.Subgraph.connected_iff SimpleGraph.Subgraph.Preconnected.map preconnected nonempty
mono 📖	—	SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.Connected	—	—	SimpleGraph.Subgraph.copy_eq SimpleGraph.Connected.mono coe
mono' 📖	—	SimpleGraph.Subgraph.Adj SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.Connected	—	—	mono Eq.le
nonempty 📖	mathematical	SimpleGraph.Subgraph.Connected	Set.Nonempty SimpleGraph.Subgraph.verts	—	SimpleGraph.Subgraph.connected_iff
preconnected 📖	mathematical	SimpleGraph.Subgraph.Connected	SimpleGraph.Subgraph.Preconnected	—	SimpleGraph.Subgraph.connected_iff
sup 📖	mathematical	SimpleGraph.Subgraph.Connected Set.Nonempty SimpleGraph.Subgraph.verts SimpleGraph.Subgraph SimpleGraph.Subgraph.instMin	SimpleGraph.Subgraph.instMax	—	SimpleGraph.Subgraph.connected_sup preconnected

SimpleGraph.Subgraph.Preconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeSubgraph 📖	mathematical	SimpleGraph.Subgraph.Preconnected Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	SimpleGraph.Subgraph.coeSubgraph	—	map
degree_zero_iff 📖	mathematical	SimpleGraph.Subgraph.Preconnected	SimpleGraph.Subgraph.degree Set Set.instMembership SimpleGraph.Subgraph.verts Set.Subsingleton	—	Set.not_nontrivial_iff Set.Nontrivial.coe_sort SimpleGraph.Subgraph.coe_degree SimpleGraph.Preconnected.degree_pos_of_nontrivial coe SimpleGraph.Subgraph.degree_eq_zero_of_subsingleton
exists_adj_of_nontrivial 📖	mathematical	SimpleGraph.Subgraph.Preconnected	SimpleGraph.Subgraph.Adj Set Set.instMembership SimpleGraph.Subgraph.verts	—	SimpleGraph.Preconnected.exists_adj_of_nontrivial coe
map 📖	mathematical	SimpleGraph.Subgraph.Preconnected Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.Subgraph.coe	SimpleGraph.Subgraph.map	—	SimpleGraph.Subgraph.preconnected_iff SimpleGraph.Reachable.coe_subgraphMap coe

SimpleGraph.Walk

Definitions

Name	Category	Theorems
mapToSubgraph 📖	CompOp	3 math math: map_mapToSubgraph_eq_induce, map_mapToSubgraph_hom, map_mapToSubgraph_eq_induce_id
toSubgraph 📖	CompOp	38 math math: edgeSet_toSubgraph, IsPath.ncard_neighborSet_toSubgraph_internal_eq_two, toSubgraph_adj_iff, toSubgraph_reverse, IsCycle.isCycles_spanningCoe_toSubgraph, SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe, toSubgraph_adj_penultimate, toSubgraph_bypass_le_toSubgraph, map_mapToSubgraph_eq_induce, adj_toSubgraph_mapLe, toSubgraph_rotate, mem_verts_toSubgraph, IsCycle.ncard_neighborSet_toSubgraph_eq_two, IsPath.neighborSet_toSubgraph_internal, IsPath.neighborSet_toSubgraph_startpoint, IsCycle.neighborSet_toSubgraph_endpoint, finite_neighborSet_toSubgraph, SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph, toSubgraph_le_iff, map_mapToSubgraph_hom, toSubgraph_adj_snd, map_mapToSubgraph_eq_induce_id, end_mem_verts_toSubgraph, toSubgraph_le_induce_support, IsPath.isCycles_spanningCoe_toSubgraph_sup_edge, toSubgraph_append, verts_toSubgraph, SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph, adj_toSubgraph_iff_mem_edges, toSubgraph_cons_nil_eq_subgraphOfAdj, toSubgraph_connected, start_mem_verts_toSubgraph, toSubgraph_adj_getVert, mem_edges_toSubgraph, SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp, IsPath.neighborSet_toSubgraph_endpoint, IsCycle.neighborSet_toSubgraph_internal, toSubgraph_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj_toSubgraph_iff_mem_edges 📖	mathematical	—	SimpleGraph.Subgraph.Adj toSubgraph Sym2 edges	—	mem_edges_toSubgraph SimpleGraph.Subgraph.mem_edgeSet
adj_toSubgraph_mapLe 📖	mathematical	SimpleGraph SimpleGraph.instLE	SimpleGraph.Subgraph.Adj toSubgraph mapLe	—	toSubgraph_map Relation.map_id_id
connected_induce_support 📖	mathematical	—	SimpleGraph.Connected Set.Elem setOf support SimpleGraph.induce	—	verts_toSubgraph SimpleGraph.Subgraph.Connected.induce_verts toSubgraph_connected
edgeSet_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph.edgeSet toSubgraph edgeSet	—	Set.ext mem_edges_toSubgraph
end_mem_verts_toSubgraph 📖	mathematical	—	Set Set.instMembership SimpleGraph.Subgraph.verts toSubgraph	—	—
exists_mem_support_forall_mem_support_imp_eq 📖	mathematical	Finset.Nonempty Finset.filter support	Finset Finset.instMembership	—	exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty Finset.instLawfulSingleton Finset.subset_insert_iff Finset.subset_empty Finset.filter_erase
exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty 📖	mathematical	Finset.Nonempty Finset.filter support	Finset Finset.instMembership takeUntil Finset.erase Finset.instEmptyCollection	—	Nat.strong_induction_on Finset.eq_empty_or_nonempty Eq.le length_takeUntil_le Finset.card_erase_add_one Finset.mem_of_mem_erase support_takeUntil_subset Finset.erase_eq_of_notMem notMem_support_takeUntil_support_takeUntil_subset Finset.filter_erase Finset.erase_right_comm takeUntil_takeUntil
finite_neighborSet_toSubgraph 📖	mathematical	—	Set.Finite SimpleGraph.Subgraph.neighborSet toSubgraph	—	toSubgraph.eq_1 SimpleGraph.neighborSet_singletonSubgraph Set.toFinite Finite.of_fintype toSubgraph.eq_2 SimpleGraph.Subgraph.neighborSet_sup Set.Finite.union Set.Finite.subset Finite.Set.finite_insert SimpleGraph.neighborSet_subgraphOfAdj_subset
map_mapToSubgraph_eq_induce 📖	mathematical	Set Set.instMembership	map Set.Elem SimpleGraph.Subgraph.verts toSubgraph SimpleGraph.Subgraph.coe SimpleGraph.induce SimpleGraph.Adj SimpleGraph.Subgraph.adj_sub start_mem_verts_toSubgraph end_mem_verts_toSubgraph mapToSubgraph induce	—	SimpleGraph.Subgraph.adj_sub start_mem_verts_toSubgraph end_mem_verts_toSubgraph mapToSubgraph.eq_2 SimpleGraph.Hom.map_adj map_cons map_map
map_mapToSubgraph_eq_induce_id 📖	mathematical	—	map Set.Elem SimpleGraph.Subgraph.verts toSubgraph support SimpleGraph.Subgraph.coe SimpleGraph.induce SimpleGraph.Adj Set Set.instMembership mem_verts_toSubgraph Subtype.prop SimpleGraph.Subgraph.adj_sub start_mem_verts_toSubgraph end_mem_verts_toSubgraph mapToSubgraph induce	—	map_mapToSubgraph_eq_induce
map_mapToSubgraph_hom 📖	mathematical	—	map Set.Elem SimpleGraph.Subgraph.verts toSubgraph SimpleGraph.Subgraph.coe SimpleGraph.Subgraph.hom Set Set.instMembership start_mem_verts_toSubgraph end_mem_verts_toSubgraph mapToSubgraph	—	start_mem_verts_toSubgraph end_mem_verts_toSubgraph mapToSubgraph.eq_2 SimpleGraph.Hom.map_adj map.eq_2 map_map
mem_edges_toSubgraph 📖	mathematical	—	Sym2 Set Set.instMembership SimpleGraph.Subgraph.edgeSet toSubgraph edges	—	SimpleGraph.edgeSet_singletonSubgraph SimpleGraph.Subgraph.edgeSet_sup SimpleGraph.edgeSet_subgraphOfAdj
mem_support_of_adj_toSubgraph 📖	mathematical	SimpleGraph.Subgraph.Adj toSubgraph	support	—	mem_verts_toSubgraph SimpleGraph.Subgraph.edge_vert
mem_verts_toSubgraph 📖	mathematical	—	Set Set.instMembership SimpleGraph.Subgraph.verts toSubgraph support	—	—
not_nil_of_adj_toSubgraph 📖	mathematical	SimpleGraph.Subgraph.Adj toSubgraph	Nil	—	—
start_mem_verts_toSubgraph 📖	mathematical	—	Set Set.instMembership SimpleGraph.Subgraph.verts toSubgraph	—	—
toSubgraph_adj_getVert 📖	mathematical	length	SimpleGraph.Subgraph.Adj toSubgraph getVert	—	getVert_zero zero_add
toSubgraph_adj_iff 📖	mathematical	—	SimpleGraph.Subgraph.Adj toSubgraph getVert length	—	toSubgraph.eq_def getVert_zero zero_add Sym2.eq_iff SimpleGraph.Subgraph.mem_edgeSet toSubgraph_adj_getVert
toSubgraph_adj_penultimate 📖	mathematical	Nil	SimpleGraph.Subgraph.Adj toSubgraph penultimate	—	not_nil_iff_lt_length getVert_length toSubgraph_adj_getVert
toSubgraph_adj_snd 📖	mathematical	Nil	SimpleGraph.Subgraph.Adj toSubgraph snd	—	getVert_zero zero_add toSubgraph_adj_getVert not_nil_iff_lt_length
toSubgraph_append 📖	mathematical	—	toSubgraph append SimpleGraph.Subgraph SimpleGraph.Subgraph.instMax	—	sup_of_le_right verts_toSubgraph sup_assoc
toSubgraph_bypass_le_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder toSubgraph bypass	—	verts_toSubgraph support_bypass_subset edges_toPath_subset
toSubgraph_connected 📖	mathematical	—	SimpleGraph.Subgraph.Connected toSubgraph	—	SimpleGraph.Subgraph.singletonSubgraph_connected SimpleGraph.Subgraph.connected_sup SimpleGraph.Subgraph.Connected.preconnected SimpleGraph.Subgraph.subgraphOfAdj_connected verts_toSubgraph
toSubgraph_cons_nil_eq_subgraphOfAdj 📖	mathematical	SimpleGraph.Adj	toSubgraph cons nil SimpleGraph.subgraphOfAdj	—	sup_of_le_left
toSubgraph_le_iff 📖	mathematical	Nil	SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder toSubgraph Set Sym2 Set.instHasSubset edgeSet SimpleGraph.Subgraph.edgeSet	—	SimpleGraph.Subgraph.edgeSet_mono mem_edges_toSubgraph mem_support_iff_exists_mem_edges_of_not_nil mem_verts_toSubgraph SimpleGraph.Subgraph.mem_verts_of_mem_edge
toSubgraph_le_induce_support 📖	mathematical	—	SimpleGraph.Subgraph Preorder.toLE PartialOrder.toPreorder SimpleGraph.Subgraph.instPartialOrder toSubgraph SimpleGraph.Subgraph.induce Top.top SimpleGraph.Subgraph.instTop setOf support	—	verts_toSubgraph SimpleGraph.Subgraph.le_induce_top_verts
toSubgraph_map 📖	mathematical	—	toSubgraph DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map SimpleGraph.Subgraph.map	—	SimpleGraph.map_singletonSubgraph SimpleGraph.Hom.map_adj SimpleGraph.Subgraph.map_sup SimpleGraph.map_subgraphOfAdj
toSubgraph_reverse 📖	mathematical	—	toSubgraph reverse	—	SimpleGraph.symm reverse_cons toSubgraph_append SimpleGraph.subgraphOfAdj_symm sup_comm SimpleGraph.Subgraph.ext Set.ext sup_of_le_left
toSubgraph_rotate 📖	mathematical	support	toSubgraph rotate	—	rotate.eq_1 toSubgraph_append sup_comm take_spec
verts_toSubgraph 📖	mathematical	—	SimpleGraph.Subgraph.verts toSubgraph setOf support	—	Set.ext mem_verts_toSubgraph

SimpleGraph.Walk.IsCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isCycle_snd_verts_eq 📖	mathematical	SimpleGraph.Walk.IsCycle SimpleGraph.Subgraph.Adj SimpleGraph.Walk.toSubgraph	SimpleGraph.Walk.snd SimpleGraph.Subgraph.verts	—	neighborSet_toSubgraph_endpoint reverse SimpleGraph.Walk.getVert_reverse SimpleGraph.Walk.penultimate.eq_1 SimpleGraph.Walk.toSubgraph_reverse
ncard_neighborSet_toSubgraph_eq_two 📖	mathematical	SimpleGraph.Walk.IsCycle SimpleGraph.Walk.support	Set.ncard SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph	—	SimpleGraph.Walk.getVert_zero SimpleGraph.Walk.getVert_length neighborSet_toSubgraph_endpoint Set.ncard_pair snd_ne_penultimate neighborSet_toSubgraph_internal getVert_sub_one_ne_getVert_add_one
neighborSet_toSubgraph_endpoint 📖	mathematical	SimpleGraph.Walk.IsCycle	SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph Set Set.instInsert SimpleGraph.Walk.snd Set.instSingletonSet SimpleGraph.Walk.penultimate	—	SimpleGraph.Walk.toSubgraph_adj_snd not_nil Set.ext
neighborSet_toSubgraph_internal 📖	mathematical	SimpleGraph.Walk.IsCycle SimpleGraph.Walk.length	SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph SimpleGraph.Walk.getVert Set Set.instInsert Set.instSingletonSet	—	SimpleGraph.Subgraph.Adj.symm SimpleGraph.Walk.toSubgraph_adj_getVert Set.ext getVert_injOn' Set.mem_setOf_eq add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid getVert_injOn

SimpleGraph.Walk.IsPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ncard_neighborSet_toSubgraph_internal_eq_two 📖	mathematical	SimpleGraph.Walk.IsPath SimpleGraph.Walk.length	Set.ncard SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph SimpleGraph.Walk.getVert	—	neighborSet_toSubgraph_internal getVert_injOn Set.mem_setOf_eq Set.ncard_insert_of_notMem Set.ncard_singleton
neighborSet_toSubgraph_endpoint 📖	mathematical	SimpleGraph.Walk.IsPath SimpleGraph.Walk.Nil	SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph Set Set.instSingletonSet SimpleGraph.Walk.penultimate	—	SimpleGraph.Walk.toSubgraph_reverse SimpleGraph.Walk.snd_reverse neighborSet_toSubgraph_startpoint reverse SimpleGraph.Walk.not_nil_iff_lt_length SimpleGraph.Walk.length_reverse
neighborSet_toSubgraph_internal 📖	mathematical	SimpleGraph.Walk.IsPath SimpleGraph.Walk.length	SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph SimpleGraph.Walk.getVert Set Set.instInsert Set.instSingletonSet	—	SimpleGraph.Subgraph.Adj.symm SimpleGraph.Walk.toSubgraph_adj_getVert Set.ext getVert_injOn Set.mem_setOf_eq add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
neighborSet_toSubgraph_startpoint 📖	mathematical	SimpleGraph.Walk.IsPath SimpleGraph.Walk.Nil	SimpleGraph.Subgraph.neighborSet SimpleGraph.Walk.toSubgraph Set Set.instSingletonSet SimpleGraph.Walk.snd	—	SimpleGraph.Walk.toSubgraph_adj_snd Set.ext
snd_of_toSubgraph_adj 📖	mathematical	SimpleGraph.Walk.IsPath SimpleGraph.Subgraph.Adj SimpleGraph.Walk.toSubgraph	SimpleGraph.Walk.snd	—	SimpleGraph.Walk.toSubgraph_adj_iff getVert_injOn Set.mem_setOf SimpleGraph.Walk.getVert_zero zero_add

---

← Back to Index