Commit 2025-10-28 13:23 0fdbde1f

View on Github →

chore: deprecate duplicate Set.dual_ordConnected_iff (#31000)

Estimated changes

Modified Mathlib/Order/Interval/Set/OrdConnected.lean

deleted theorem Set.dual_ordConnected_iff