Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-05 21:00 7221900b

View on Github →

feat(data/set/basic): more lemmas about set.nonempty (#1780)

  • feat(data/set/basic): more lemmas about set.nonempty
  • Fix compile

Estimated changes

added theorem set.insert_nonempty
added theorem set.nonempty.ne_empty
modified theorem set.singleton_ne_empty
added theorem set.singleton_nonempty