Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-27 00:09 894f92bc

View on Github →

refactor(order/upper_lower): Reverse the order on upper_set (#14982) Having upper_set being ordered by reverse inclusion makes it order-isomorphic to lower_set (and antichains once we have them as a type) and it matches the order on filter.

Estimated changes

modified theorem upper_set.Ici_Sup
modified def upper_set.Ici_Sup_hom
added theorem upper_set.Ici_bot
modified theorem upper_set.Ici_sup
modified def upper_set.Ici_sup_hom
modified theorem upper_set.Ici_sup_hom_apply
modified theorem upper_set.Ici_supr
modified theorem upper_set.Ici_supr₂
deleted theorem upper_set.Ici_top
added theorem upper_set.Icoi_le_Ioi
deleted theorem upper_set.Ioi_bot
deleted theorem upper_set.Ioi_le_Ici
added theorem upper_set.Ioi_top
modified theorem upper_set.coe_Inf
modified theorem upper_set.coe_Sup
modified theorem upper_set.coe_bot
modified theorem upper_set.coe_inf
modified theorem upper_set.coe_infi
modified theorem upper_set.coe_infi₂
modified theorem upper_set.coe_sup
modified theorem upper_set.coe_supr
modified theorem upper_set.coe_supr₂
modified theorem upper_set.coe_top
modified theorem upper_set.mem_Inf_iff
modified theorem upper_set.mem_Sup_iff
added theorem upper_set.mem_bot
modified theorem upper_set.mem_inf_iff
modified theorem upper_set.mem_infi_iff
modified theorem upper_set.mem_infi₂_iff
modified theorem upper_set.mem_sup_iff
modified theorem upper_set.mem_supr_iff
modified theorem upper_set.mem_supr₂_iff
deleted theorem upper_set.mem_top
deleted theorem upper_set.not_mem_bot
added theorem upper_set.not_mem_top