Commit 2025-06-25 10:16 17fbb005

View on Github →

feat(Set/Monotone): convenience special cases for monotonicity on insert (#26369) Add four special case lemmas to describe monotonicity on insert in the case where the new element is above or below all existing ones. Also make better use of variable.

Estimated changes

Modified Mathlib/Data/Set/Monotone.lean

modified theorem StrictMono.codRestrict

modified theorem strictAntiOn_insert_iff

added theorem strictAntiOn_insert_iff_of_forall_ge

added theorem strictAntiOn_insert_iff_of_forall_le

modified theorem strictMonoOn_insert_iff

added theorem strictMonoOn_insert_iff_of_forall_ge

added theorem strictMonoOn_insert_iff_of_forall_le

modified theorem strictMono_restrict