Commit 2025-06-14 08:57 b91260d8

View on Github →

chore: fix capitalization of two lemmas (#25853)

Estimated changes

Modified Mathlib/Data/Set/Monotone.lean

deleted theorem Set.AntitoneOn_insert_iff

deleted theorem Set.MonotoneOn_insert_iff

added theorem Set.antitoneOn_insert_iff

added theorem Set.monotoneOn_insert_iff