Mathlib Changelog
v4
Changelog
About
Github
Theorem
strictMonoOn_insert_iff_of_forall_le
Modification history
2025-06-25 10:16
Mathlib/Data/Set/Monotone.lean
feat(Set/Monotone): convenience special cases for monotonicity on insert (#26369) …
Added
strictMonoOn_insert_iff_of_forall_le
View on Github →