Commit 2021-07-14 17:41 e9b1fbd0

View on Github →

feat(combinatorics/simple_graph): add maps and subgraphs (#8223) Add graph homomorphisms, isomorphisms, and embeddings. Define subgraphs and supporting lemmas and definitions. Also renamed edge_symm to adj_comm.

Estimated changes

Modified src/combinatorics/simple_graph/adj_matrix.lean

Modified src/combinatorics/simple_graph/basic.lean

added def empty_graph

added theorem simple_graph.adj_comm

added theorem simple_graph.adj_symm

deleted theorem simple_graph.edge_symm'

deleted theorem simple_graph.edge_symm

added theorem simple_graph.embedding.apply_mem_neighbor_set_iff

added theorem simple_graph.embedding.coe_comp

added def simple_graph.embedding.comp

added theorem simple_graph.embedding.map_adj_iff

added def simple_graph.embedding.map_edge_set

added theorem simple_graph.embedding.map_mem_edge_set_iff

added def simple_graph.embedding.map_neighbor_set

added def simple_graph.embedding.refl

added def simple_graph.embedding.to_hom

added def simple_graph.embedding

added theorem simple_graph.hom.apply_mem_neighbor_set

added theorem simple_graph.hom.coe_comp

added def simple_graph.hom.comp

added def simple_graph.hom.id

added theorem simple_graph.hom.map_adj

added theorem simple_graph.hom.map_edge_set.injective

added def simple_graph.hom.map_edge_set

added theorem simple_graph.hom.map_mem_edge_set

added def simple_graph.hom.map_neighbor_set

added def simple_graph.hom

added theorem simple_graph.iso.apply_mem_neighbor_set_iff

added theorem simple_graph.iso.card_eq_of_iso

added theorem simple_graph.iso.coe_comp

added def simple_graph.iso.comp

added theorem simple_graph.iso.map_adj_iff

added def simple_graph.iso.map_edge_set

added theorem simple_graph.iso.map_mem_edge_set_iff

added def simple_graph.iso.map_neighbor_set

added def simple_graph.iso.refl

added def simple_graph.iso.symm

added def simple_graph.iso.to_embedding

added def simple_graph.iso.to_hom

added def simple_graph.iso

Created src/combinatorics/simple_graph/subgraph.lean

added theorem simple_graph.subgraph.adj_comm

added theorem simple_graph.subgraph.adj_symm

added def simple_graph.subgraph.bot

added def simple_graph.subgraph.bot_equiv

added def simple_graph.subgraph.coe

added theorem simple_graph.subgraph.coe_adj_sub

added theorem simple_graph.subgraph.coe_degree

added def simple_graph.subgraph.coe_neighbor_set_equiv

added def simple_graph.subgraph.copy

added theorem simple_graph.subgraph.copy_eq

added def simple_graph.subgraph.degree

added theorem simple_graph.subgraph.degree_le'

added theorem simple_graph.subgraph.degree_le

added def simple_graph.subgraph.edge_set

added theorem simple_graph.subgraph.edge_set_subset

added def simple_graph.subgraph.finite_at_of_subgraph

added def simple_graph.subgraph.incidence_set

added theorem simple_graph.subgraph.incidence_set_subset

added theorem simple_graph.subgraph.incidence_set_subset_incidence_set

added def simple_graph.subgraph.inter

added def simple_graph.subgraph.is_induced

added def simple_graph.subgraph.is_spanning

added def simple_graph.subgraph.is_subgraph

added theorem simple_graph.subgraph.map.injective

added def simple_graph.subgraph.map

added theorem simple_graph.subgraph.map_top.injective

added def simple_graph.subgraph.map_top

added theorem simple_graph.subgraph.map_top_to_fun

added theorem simple_graph.subgraph.mem_edge_set

added theorem simple_graph.subgraph.mem_neighbor_set

added theorem simple_graph.subgraph.mem_verts_if_mem_edge

added def simple_graph.subgraph.neighbor_set

added theorem simple_graph.subgraph.neighbor_set_subset

added theorem simple_graph.subgraph.neighbor_set_subset_of_subgraph

added def simple_graph.subgraph.top

added def simple_graph.subgraph.top_equiv

added def simple_graph.subgraph.union

added def simple_graph.subgraph.vert

added structure simple_graph.subgraph

Modified src/data/sym2.lean

added theorem sym2.map.injective

added theorem sym2.map_map

modified theorem sym2.map_pair_eq