Theorem biSup_le_eq_of_monotone

Modification history

2025-03-17 20:24

Mathlib/Order/CompleteLattice.lean

feat: biSup and biInf for monotone and antitone functions (#22560)

Added biSup_le_eq_of_monotone View on Github →