Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-04 12:04 3669cb35

View on Github →

feat(data/real/ennreal): add ennreal.prod_lt_top (#5602) Also add with_top.can_lift, with_top.mul_lt_top, and with_top.prod_lt_top.

Estimated changes

Modified src/algebra/big_operators/order.lean

added theorem with_top.prod_lt_top

Modified src/algebra/ordered_ring.lean

added theorem with_top.mul_lt_top

Modified src/data/real/ennreal.lean

added theorem ennreal.prod_lt_top

Modified src/order/bounded_lattice.lean