Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-01 11:03 e876965f

View on Github →

chore(combinatorics/simple_graph/connectivity): open a namespace block for connected_component (#18520)

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

modified def simple_graph.connected_component.map

modified theorem simple_graph.connected_component.map_comp

modified theorem simple_graph.connected_component.map_id

modified theorem simple_graph.connected_component.map_mk

modified theorem simple_graph.preconnected.subsingleton_connected_component