Maps

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

Statistics

Metric	Count
Definitions induce, map, mapLe, toDeleteEdge, toDeleteEdges, transfer	6
Theorems darts_map, edgeSet_map, edgeSet_mapLe_eq_edgeSet, edgeSet_transfer, edges_map, edges_mapLe_eq_edges, edges_transfer, getVert_map, induce_cons, induce_nil, length_map, length_transfer, map_append, map_cons, map_copy, map_eq_nil_iff, map_eq_of_eq, map_id, map_induce, map_induce_induceHomOfLE, map_injective_of_injective, map_map, map_nil, map_toDeleteEdges_eq, reverse_map, reverse_transfer, support_induce, support_map, support_mapLe_eq_support, support_transfer, toDeleteEdges_cons, toDeleteEdges_nil, transfer_append, transfer_eq_map_ofLE, transfer_self, transfer_transfer	36
Total	42

SimpleGraph.Walk

Definitions

Name	Category	Theorems
induce 📖	CompOp	7 math math: map_induce_induceHomOfLE, map_mapToSubgraph_eq_induce, induce_cons, map_mapToSubgraph_eq_induce_id, support_induce, induce_nil, map_induce
map 📖	CompOp	35 math math: map_copy, map_injective_of_injective, SimpleGraph.Path.mapEmbedding_coe, transfer_eq_map_ofLE, IsCycle.map, map_toDeleteEdges_eq, map_induce_induceHomOfLE, map_isCycle_iff_of_injective, map_mapToSubgraph_eq_induce, darts_map, map_nil, map_map, IsHamiltonian.map, map_isPath_iff_of_injective, IsSubwalk.map, map_id, map_mapToSubgraph_hom, reverse_map, map_mapToSubgraph_eq_induce_id, length_map, map_isTrail_iff_of_injective, map_isTrail_of_injective, map_cons, map_isPath_of_injective, edgeSet_map, SimpleGraph.Path.map_coe, map_append, map_eq_of_eq, map_induce, support_map, IsHamiltonianCycle.map, edges_map, map_eq_nil_iff, getVert_map, toSubgraph_map
mapLe 📖	CompOp	10 math math: edges_mapLe_eq_edges, mapLe_isPath, adj_toSubgraph_mapLe, IsCycle.mapLe, IsPath.mapLe, IsTrail.mapLe, edgeSet_mapLe_eq_edgeSet, mapLe_isTrail, mapLe_isCycle, support_mapLe_eq_support
toDeleteEdge 📖	CompOp	—
toDeleteEdges 📖	CompOp	6 math math: map_toDeleteEdges_eq, IsCycle.toDeleteEdges, toDeleteEdges_copy, IsPath.toDeleteEdges, toDeleteEdges_cons, toDeleteEdges_nil
transfer 📖	CompOp	11 math math: transfer_eq_map_ofLE, support_transfer, edges_transfer, reverse_transfer, transfer_transfer, IsCycle.transfer, IsPath.transfer, transfer_append, length_transfer, transfer_self, edgeSet_transfer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
darts_map 📖	mathematical	—	darts DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map SimpleGraph.Dart SimpleGraph.Hom.mapDart	—	SimpleGraph.Hom.map_adj SimpleGraph.Dart.adj
edgeSet_map 📖	mathematical	—	edgeSet DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map Set.image Sym2 Sym2.map	—	Set.ext edges_map
edgeSet_mapLe_eq_edgeSet 📖	mathematical	SimpleGraph SimpleGraph.instLE	edgeSet mapLe	—	edgeSet_map Set.image_congr Sym2.map_congr Sym2.map_id' Set.image_id'
edgeSet_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	edgeSet transfer	—	Set.ext edges_transfer
edges_map 📖	mathematical	—	edges DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map Sym2 Sym2.map	—	—
edges_mapLe_eq_edges 📖	mathematical	SimpleGraph SimpleGraph.instLE	edges mapLe	—	edges_map Sym2.map_id
edges_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	edges transfer	—	—
getVert_map 📖	mathematical	—	getVert DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map	—	getVert_zero SimpleGraph.Hom.map_adj
induce_cons 📖	mathematical	SimpleGraph.Adj Set Set.instMembership	induce cons Set.Elem SimpleGraph.induce start_mem_support end_mem_support SimpleGraph.induce_adj	—	start_mem_support end_mem_support
induce_nil 📖	mathematical	Set Set.instMembership	induce nil Set.Elem SimpleGraph.induce start_mem_support	—	start_mem_support end_mem_support
length_map 📖	mathematical	—	length DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map	—	—
length_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	length transfer	—	—
map_append 📖	mathematical	—	map append DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	—	SimpleGraph.Hom.map_adj cons.congr_simp
map_cons 📖	mathematical	SimpleGraph.Adj	map cons DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Hom.map_adj	—	—
map_copy 📖	mathematical	—	map copy DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	—	—
map_eq_nil_iff 📖	mathematical	—	map nil DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	—	SimpleGraph.Hom.map_adj
map_eq_of_eq 📖	mathematical	—	map copy DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	—	—
map_id 📖	mathematical	—	map SimpleGraph.Hom.id	—	SimpleGraph.Hom.map_adj cons.congr_simp
map_induce 📖	mathematical	Set Set.instMembership	map Set.Elem SimpleGraph.induce SimpleGraph.Embedding.toHom SimpleGraph.Embedding.induce start_mem_support end_mem_support induce	—	start_mem_support end_mem_support SimpleGraph.Hom.map_adj SimpleGraph.induce_adj cons.congr_simp
map_induce_induceHomOfLE 📖	mathematical	Set Set.instHasSubset Set.instMembership	map Set.Elem SimpleGraph.induce SimpleGraph.Embedding.toHom SimpleGraph.induceHomOfLE start_mem_support end_mem_support induce subset_trans Set.instIsTransSubset support	—	start_mem_support end_mem_support subset_trans Set.instIsTransSubset SimpleGraph.induce_adj SimpleGraph.Hom.map_adj cons.congr_simp
map_injective_of_injective 📖	mathematical	DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	SimpleGraph.Walk map	—	SimpleGraph.Hom.map_adj
map_map 📖	mathematical	—	map DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj SimpleGraph.Hom.comp	—	SimpleGraph.Hom.map_adj cons.congr_simp
map_nil 📖	mathematical	—	map nil DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj	—	—
map_toDeleteEdges_eq 📖	mathematical	Sym2 Set Set.instMembership	map SimpleGraph.deleteEdges SimpleGraph.Hom.ofLE SimpleGraph.deleteEdges_le toDeleteEdges	—	SimpleGraph.deleteEdges_le edges_subset_edgeSet edges_transfer transfer_eq_map_ofLE transfer_transfer transfer_self
reverse_map 📖	mathematical	—	reverse DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map	—	SimpleGraph.symm SimpleGraph.Hom.map_adj reverse_cons map_append
reverse_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	reverse transfer	—	SimpleGraph.symm reverse_cons transfer.congr_simp transfer_append
support_induce 📖	mathematical	Set Set.instMembership	support Set.Elem SimpleGraph.induce start_mem_support end_mem_support induce	—	start_mem_support end_mem_support
support_map 📖	mathematical	—	support DFunLike.coe SimpleGraph.Hom RelHom.instFunLike SimpleGraph.Adj map	—	—
support_mapLe_eq_support 📖	mathematical	SimpleGraph SimpleGraph.instLE	support mapLe	—	support_map
support_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	support transfer	—	—
toDeleteEdges_cons 📖	mathematical	SimpleGraph.Adj Sym2 Set Set.instMembership	toDeleteEdges cons SimpleGraph.deleteEdges SimpleGraph.deleteEdges_adj SimpleGraph.Dart SimpleGraph.Dart.edge darts	—	—
toDeleteEdges_nil 📖	mathematical	Sym2 Set Set.instMembership	toDeleteEdges nil SimpleGraph.deleteEdges	—	—
transfer_append 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	transfer append	—	cons.congr_simp
transfer_eq_map_ofLE 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet SimpleGraph SimpleGraph.instLE	transfer map SimpleGraph.Hom.ofLE	—	SimpleGraph.Hom.map_adj cons.congr_simp
transfer_self 📖	mathematical	—	transfer edges_subset_edgeSet	—	edges_subset_edgeSet cons.congr_simp
transfer_transfer 📖	mathematical	Sym2 Set Set.instMembership SimpleGraph.edgeSet	transfer edges edges_transfer	—	edges_transfer cons.congr_simp

---

← Back to Index