Theorem strictMonoOn_insert_iff

Modification history

2025-06-25 10:16
Mathlib/Data/Set/Monotone.lean
feat(Set/Monotone): convenience special cases for monotonicity on insert (#26369) …
Modified strictMonoOn_insert_iffView on Github →
2024-10-07 17:59
Mathlib/Data/Set/Monotone.lean
feat(Data/Set): monotonicity on insert (#17086)
Added strictMonoOn_insert_iffView on Github →