Theorem SimpleGraph.IsBridge.anti_of_mem_edgeSet

Modification history

2026-06-05 15:27

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

refactor(SimpleGraph): change bridges not to require the edge to be present (#32583) …

Deleted SimpleGraph.IsBridge.anti_of_mem_edgeSet View on Github →

2025-11-16 02:02

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

feat(Combinatorics/SimpleGraph/Connectivity/Connected): `IsBridge` is antitone (#30639)

Added SimpleGraph.IsBridge.anti_of_mem_edgeSet View on Github →