Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lower_set.coe_prod

Modification history

2022-12-05 14:00
src/order/upper_lower.lean
feat(order/upper_lower): More `prod` lemmas (#17747) …
Modified lower_set.coe_prodView on Github →
2022-11-29 03:00
src/order/upper_lower.lean
feat(order/upper_lower): `×ˢ` notation for upper/lower sets (#17746) …
Modified lower_set.coe_prodView on Github →
2022-10-17 04:40
src/order/upper_lower.lean
feat(order/upper_lower): Product of upper sets (#17022) …
Added lower_set.coe_prodView on Github →