Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 13:51 dcd5ebd9

View on Github →

feat({data/{finset,set},order/filter}/pointwise): More lemmas (#14216) Lemmas about s ^ n, 0 * s and 1 ∈ s / t. Other changes:

  • finset.mul_card_le → finset.card_mul_le
  • finset.card_image_eq_iff_inj_on → finset.card_image_iff.
  • zero_smul_subset → zero_smul_set_subset
  • Reorder lemmas slightly
  • Add an explicit argument to finset.coe_smul_finset
  • Remove an explicit argument to set.empty

Estimated changes

added theorem finset.card_image_iff
added theorem finset.card_mul_iff
added theorem finset.card_mul_le
added theorem finset.empty_pow
added theorem finset.image_div
added theorem finset.image_mul
modified theorem finset.image_one
deleted theorem finset.mul_card_le
added theorem finset.one_mem_div_iff
added theorem finset.pow_mem_pow
added theorem finset.pow_subset_pow
added theorem finset.subset_mul_left
added theorem finset.univ_mul_univ
added theorem finset.univ_pow
added theorem set.div_zero_subset
modified theorem set.empty_pow
added theorem set.image_div
modified theorem set.image_mul
added theorem set.mul_zero_subset
added theorem set.nonempty.div_zero
added theorem set.nonempty.mul_zero
added theorem set.nonempty.smul_zero
added theorem set.nonempty.zero_div
added theorem set.nonempty.zero_mul
added theorem set.nonempty.zero_smul
added theorem set.nsmul_univ
added theorem set.one_mem_div_iff
modified theorem set.smul_mem_smul_set_iff
added theorem set.smul_zero_subset
added theorem set.univ_pow
added theorem set.zero_div_subset
added theorem set.zero_mul_subset
modified theorem set.zero_smul_subset
modified theorem filter.le_def
added theorem filter.le_map_iff
added theorem filter.ne_bot.of_map
added theorem filter.bot_pow
added theorem filter.mem_mul
deleted theorem filter.mem_mul_iff
added theorem filter.nsmul_top
added theorem filter.top_mul_top
added theorem filter.top_pow