Commit 2024-10-06 14:52 eb8e7ea5

View on Github →

chore: let gcongr know about piecewise (#17468)

Estimated changes

Modified Mathlib/Data/Set/Function.lean

deleted theorem Set.piecewise_le_piecewise

added theorem Set.piecewise_mono