Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-07 11:52 d6e84a0d

View on Github →

feat(combinatorics/simple_graph/connectivity): walk.to_subgraph (#17325) A construction for the subgraph consisting of the vertices and edges of a given walk.

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added theorem simple_graph.walk.edge_set_to_subgraph

added theorem simple_graph.walk.finite_neighbor_set_to_subgraph

added theorem simple_graph.walk.mem_edges_to_subgraph

added theorem simple_graph.walk.mem_verts_to_subgraph

added theorem simple_graph.walk.support_nonempty

added theorem simple_graph.walk.to_subgraph_append

added theorem simple_graph.walk.to_subgraph_cons_nil_eq_subgraph_of_adj

added theorem simple_graph.walk.to_subgraph_map

added theorem simple_graph.walk.to_subgraph_reverse

added theorem simple_graph.walk.to_subgraph_rotate

added theorem simple_graph.walk.verts_to_subgraph

Modified src/combinatorics/simple_graph/subgraph.lean

added theorem simple_graph.subgraph.map_sup

added theorem simple_graph.subgraph.neighbor_set_inf

added theorem simple_graph.subgraph.neighbor_set_sup

added theorem simple_graph.subgraph.verts_inf

added theorem simple_graph.subgraph.verts_sup