Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-05 01:31 324ae4b1

View on Github →

feat(data/set/basic): define set.nonempty (#1779)

  • Define set.nonempty and prove some basic lemmas
  • Migrate well_founded.min to set.nonempty
  • Fix a docstring and a few names Based on comments in PR
  • More docs
  • Linebreaks
  • +2 docstrings
  • Fix compile
  • Fix compile of archive/imo1988_q6

Estimated changes

modified theorem set.empty_prod
modified theorem set.ne_empty_iff_exists_mem
added theorem set.nonempty.fst
added theorem set.nonempty.inl
added theorem set.nonempty.inr
added theorem set.nonempty.left
added theorem set.nonempty.of_diff
added theorem set.nonempty.of_subset
added theorem set.nonempty.prod
added theorem set.nonempty.right
added theorem set.nonempty.snd
added theorem set.nonempty_of_mem
modified theorem set.prod_empty
added theorem set.prod_ne_empty_iff
deleted theorem set.prod_neq_empty_iff
added theorem set.prod_nonempty_iff
added theorem set.union_nonempty
added theorem set.univ_nonempty