Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 01:29 cb948930

View on Github →

refactor(order/complete_lattice): Sup lemmas before Inf lemmas (#14868) Throughout the file, we make sure that Sup theorems always appear immediately before their Inf counterparts. This ensures consistency, and makes it much easier to golf theorems or detect missing API. We choose to put Sup before Inf rather than the other way around, since this seems to minimize the amount of things that need to be moved around, and it matches the order that we define the two operations. We also golf a few proofs throughout, and add some missing corresponding theorems, namely:

  • infi_extend_top
  • infi_supr_ge_nat_add
  • unary_relation_Inf_iff
  • binary_relation_Inf_iff

Estimated changes

modified theorem Inf_eq_top
modified theorem Inf_image
modified theorem Sup_apply
modified theorem Sup_eq_bot
modified theorem Sup_eq_top
modified theorem Sup_image
modified theorem inf_infi
modified theorem infi_and
modified theorem infi_const
modified theorem infi_emptyset
modified theorem infi_eq_bot
modified theorem infi_exists
added theorem infi_extend_top
modified theorem infi_image
modified theorem infi_inf
modified theorem infi_inf_eq
modified theorem infi_le_infi_of_subset
modified theorem infi_option
modified theorem infi_prod
modified theorem infi_range
modified theorem infi_sigma
modified theorem infi_split
modified theorem infi_split_single
modified theorem infi_subtype''
modified theorem infi_subtype
modified theorem infi_sum
added theorem infi_supr_ge_nat_add
modified theorem infi_top
modified theorem infi_union
modified theorem infi_univ
modified theorem le_infi_const
modified theorem sup_supr
modified theorem supr_and
modified theorem supr_bot
modified theorem supr_const
modified theorem supr_const_le
modified theorem supr_emptyset
modified theorem supr_eq_top
modified theorem supr_exists
modified theorem supr_le_supr_of_subset
modified theorem supr_option
modified theorem supr_prod
modified theorem supr_sigma
modified theorem supr_split_single
modified theorem supr_subtype''
modified theorem supr_subtype'
modified theorem supr_subtype
modified theorem supr_sum
modified theorem supr_sup
modified theorem supr_sup_eq
modified theorem supr_univ
added theorem unary_relation_Inf_iff