Theorem biInf_le_eq_of_antitone

Modification history

2025-03-17 20:24

Mathlib/Order/CompleteLattice.lean

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

Added biInf_le_eq_of_antitone View on Github →