Commit 2025-10-29 16:18 5c26ea9e

View on Github →

feat(Combinatorics/SimpleGraph/Connectivity/WalkCounting): a spanning subgraph has the same or more connected components (#30354)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.ConnectedComponent.surjective_map_ofLE

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

added theorem SimpleGraph.ConnectedComponent.card_le_card_of_le