Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-13 22:32 3310acfa

View on Github →

feat(order/bounds/basic): add is_greatest_univ_iff etc (#18162) Also add ae_measurable_const' and golf 2 proofs.

Estimated changes

added theorem ae_measurable_const'
modified theorem is_glb_empty
added theorem is_glb_empty_iff
modified theorem is_glb_univ
modified theorem is_greatest_univ
added theorem is_greatest_univ_iff
modified theorem is_least_univ
added theorem is_least_univ_iff
modified theorem is_lub_empty
added theorem is_lub_empty_iff
modified theorem is_lub_univ