Commit 2025-05-04 09:21 9c5455a1

View on Github →

feat(Combinatorics/SimpleGraph): Add SimpleGraph.Preconnected.support_eq_univ (#22050)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Preconnected.support_eq_univ

added theorem SimpleGraph.adj_of_mem_walk_support

added theorem SimpleGraph.mem_support_of_mem_walk_support

added theorem SimpleGraph.mem_support_of_reachable