Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-05 14:00 97b62c86

View on Github →

feat(order/upper_lower): More prod lemmas (#17747) Transfer more set lemmas about prod to upper_set/lower_set lemmas.

Estimated changes

added theorem set.prod_mono_left
added theorem set.prod_mono_right
modified theorem lower_set.bot_prod
added theorem lower_set.coe_eq_empty
added theorem lower_set.coe_eq_univ
modified theorem lower_set.coe_prod
added theorem lower_set.disjoint_coe
added theorem lower_set.inf_prod
modified def lower_set.prod
modified theorem lower_set.prod_bot
added theorem lower_set.prod_eq_bot
added theorem lower_set.prod_inf
added theorem lower_set.prod_mono
added theorem lower_set.prod_sup
added theorem lower_set.sup_prod
added theorem upper_set.coe_eq_empty
added theorem upper_set.coe_eq_univ
modified theorem upper_set.coe_prod
added theorem upper_set.inf_prod
modified def upper_set.prod
added theorem upper_set.prod_eq_top
added theorem upper_set.prod_inf
added theorem upper_set.prod_mono
added theorem upper_set.prod_sup
modified theorem upper_set.prod_top
added theorem upper_set.sup_prod
modified theorem upper_set.top_prod