connectivity): `walk.to_subgraph` (#17325)

Commit

2 years ago

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

Author

kmill

Parents

10708587

mathlib d6e84a0d - feat(combinatorics/simple_graph/connectivity): `walk.to_subgraph` (#17325)

mathlib
d6e84a0d - feat(combinatorics/simple_graph/connectivity): `walk.to_subgraph` (#17325)