Commit 2024-10-07 17:59 71c35205

View on Github →

feat(Data/Set): monotonicity on insert (#17086)

Estimated changes

Modified Mathlib/Data/Set/Monotone.lean

added theorem Set.AntitoneOn_insert_iff

added theorem Set.MonotoneOn_insert_iff

added theorem strictAntiOn_insert_iff

added theorem strictMonoOn_insert_iff