Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 17:32 cbf3062b

View on Github →

feat(combinatorics/simple_graph/connectivity): define connected components (#12766)

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added def simple_graph.connected_component

added def simple_graph.connected_component_mk

added theorem simple_graph.preconnected.subsingleton_connected_component

modified def simple_graph.subgraph.connected