Commit 2023-01-25 10:48 e1e5bf4c

View on Github →

Feat: add isLeast_univ_iff etc (#1549) This is a forward-port of leanprover-community/mathlib#18162

Estimated changes

modified theorem isGLB_empty
added theorem isGLB_empty_iff
modified theorem isGLB_univ
modified theorem isGreatest_univ
added theorem isGreatest_univ_iff
modified theorem isLUB_empty
added theorem isLUB_empty_iff
modified theorem isLUB_univ
modified theorem isLeast_univ
added theorem isLeast_univ_iff