Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 17:40 7802ba77

View on Github →

refactor(data/set/basic): review API of set.nontrivial (#16737)

  • make z an explicit argument in set.nontrivial.exists_ne;
  • rename set.nontrivial.iff_exists_lt to set.nontrivial_iff_exists_lt;
  • protect lemmas set.nontrivial.nonempty and set.nontrivial.ne_empty.

Estimated changes

modified theorem set.nontrivial.exists_ne
deleted theorem set.nontrivial.ne_empty
deleted theorem set.nontrivial.nonempty