Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-28 12:51 78bc3724

View on Github →

feat(data/{finset, set}/basic): tweak nonempty_coe_sort and is_empty_coe_sort (#14937) This PR does the following:

  • add lemmas set.is_empty_coe_sort and finset.is_empty_coe_sort
  • made argument of both nonempty_coe_sort lemmas inferred
  • fix some spacing

Estimated changes

modified theorem finset.coe_nonempty
modified theorem finset.nonempty.bex
modified theorem finset.nonempty_coe_sort
added theorem set.is_empty_coe_sort
modified theorem set.nonempty_coe_sort