Commit 2023-07-12 10:05 9f063747

View on Github →

feat(Order.Bounds.Basic): boundedness in pi types (#5806)

Estimated changes

added theorem bddAbove_pi
added theorem bddAbove_range_pi
added theorem bddBelow_pi
added theorem bddBelow_range_pi
modified theorem isGLB_pi
modified theorem isLUB_pi