Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-26 01:12 9decec2b

View on Github →

feat(*): some simple lemmas about sets and finite sets (#1903)

  • feat(*): some simple lemmas about sets and finite sets
  • More lemmas, simplify proofs
  • Introduce finsup.nonempty and use it.
  • Update src/algebra/big_operators.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com
  • Revert "Update src/algebra/big_operators.lean" This reverts commit 17c89a808545203dc5a80a4f11df4f62e949df8d. It breaks compile if we rewrite right to left.
  • simp, to_additive
  • Add a missing docstring

Estimated changes

modified theorem finset.prod_Ico_id_eq_fact
added theorem finset.sum_lt_sum
modified theorem finset.sum_const'
modified theorem finset.card_pos
added theorem finset.coe_nonempty
modified theorem finset.exists_min
modified theorem finset.image_const
modified def finset.max'
deleted theorem finset.max_of_ne_empty
added theorem finset.max_of_nonempty
modified def finset.min'
deleted theorem finset.min_of_ne_empty
added theorem finset.min_of_nonempty
added theorem finset.nonempty.bex
added theorem finset.nonempty.image
added theorem finset.nonempty.mono
modified def finsupp.split_support
added theorem fin.prod_univ_succ
added theorem fin.prod_univ_zero
added theorem fin.sum_univ_succ
added theorem fin.univ_succ
modified theorem set.exists_min
added theorem set.Inter_subset_Inter
modified theorem set.Union_subset_iff
modified theorem set.mem_Inter_of_mem
modified theorem set.subset_Inter