Theorem SimpleGraph.ConnectedComponent.card_le_card_of_le

Modification history

2026-03-18 23:07
Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean
chore(Combinatorics/SimpleGraph): move `WalkDecomp` and `WalkCounting` to `Walks` (#36819) …
Modified SimpleGraph.ConnectedComponent.card_le_card_of_leView on Github →
2025-10-29 16:18
Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
feat(Combinatorics/SimpleGraph/Connectivity/WalkCounting): a spanning subgraph has the same or more connected components (#30354)
Added SimpleGraph.ConnectedComponent.card_le_card_of_leView on Github →