Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_glb_upper_bounds

Modification history

2021-08-09 13:47

src/order/bounds.lean

feat(order/bounds): `is_lub`/`is_glb` in Pi types and product types (#8583) …

Added is_glb_upper_bounds View on Github →