Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-02 10:49 58899d43

View on Github →

feat(data/set/basic): define set.subsingleton (#1939)

  • feat(data/set/basic): define set.subsingleton Also rename nonempty.of_subset to nonempty.mono
  • Add a missing lemma

Estimated changes

added theorem set.bex_insert_iff
added theorem set.image_pair
added theorem set.nonempty.image
added theorem set.nonempty.mono
added theorem set.nonempty.of_image
deleted theorem set.nonempty.of_ssubset'
deleted theorem set.nonempty.of_subset
deleted theorem set.nonempty_image
added theorem set.nonempty_image_iff
added theorem set.subset_diff_union
deleted theorem set.subset_insert_diff
added theorem set.subsingleton.image
added theorem set.subsingleton_empty