Commit 2025-06-08 14:55 d1c754c2

View on Github →

feat(Combinatorics/SimpleGraph): introduce ConnectedComponent.toSimpleGraph (#22085)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

deleted theorem SimpleGraph.IsCycles.induce_supp

added theorem SimpleGraph.IsCycles.toSimpleGraph

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

deleted theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_induce_supp

added theorem SimpleGraph.ConnectedComponent.adj_spanningCoe_toSimpleGraph

deleted theorem SimpleGraph.ConnectedComponent.connected_induce_supp

added theorem SimpleGraph.ConnectedComponent.connected_toSimpleGraph

modified theorem SimpleGraph.ConnectedComponent.map_id

added theorem SimpleGraph.ConnectedComponent.mem_supp_of_adj_mem_supp

deleted theorem SimpleGraph.ConnectedComponent.reachable_induce_supp

added theorem SimpleGraph.ConnectedComponent.reachable_of_mem_supp

added theorem SimpleGraph.ConnectedComponent.reachable_toSimpleGraph

added def SimpleGraph.ConnectedComponent.toSimpleGraph

added theorem SimpleGraph.ConnectedComponent.toSimpleGraph_adj

added def SimpleGraph.ConnectedComponent.toSimpleGraph_hom

added theorem SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean