Commit 2025-01-30 18:56 3d895fb3

View on Github →

feat: iff version of le_of_forall_le (#21264) Also rename le_of_forall_le' to le_of_forall_ge.

Estimated changes

added theorem forall_le_iff_ge
added theorem forall_le_iff_le
added theorem le_of_forall_ge
deleted theorem le_of_forall_le'