Commit 2026-04-01 13:03 4e83c735

View on Github →

refactor(Combinatorics/SimpleGraph): use edge and deleteEdges more (#36804) Alternatively, we should make them abbrevs.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

deleted theorem SimpleGraph.IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable

added theorem SimpleGraph.IsAcyclic.sup_edge_of_not_reachable

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.le_fromEdgeSet_iff

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

added theorem SimpleGraph.IsBridge.of_not_reachable

added theorem SimpleGraph.IsBridge.sup_edge_of_not_reachable

added theorem SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridge

deleted theorem SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable

deleted theorem SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable_of_isBridge

added theorem SimpleGraph.reachable_deleteEdges_iff_exists_walk

deleted theorem SimpleGraph.reachable_delete_edges_iff_exists_walk

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

added theorem SimpleGraph.deleteEdges_eq_bot

added theorem SimpleGraph.deleteEdges_le_iff

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

added theorem SimpleGraph.deleteEdges_edge

added theorem SimpleGraph.edgeSet_edge

added theorem SimpleGraph.edgeSet_edge_of_ne

added theorem SimpleGraph.edgeSet_edge_subset

deleted theorem SimpleGraph.edge_edgeSet_of_ne

added theorem SimpleGraph.edge_le