Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 13:24 1d7f4798

View on Github →

feat(data/set/basic): Add set.nontrivial predicate and API (#15867) Analogously to the existing set.subsingleton, we add set.nontrivial and the corresponding API. This allows for dot notation to be used for set.nontrivial (which is equivalent to ¬ set.subsingleton). We also make some small changes to set.subsingleton, mostly style tweaks, a rename, and a missing lemma.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.nontrivial.exists_lt

added theorem set.nontrivial.exists_ne

added theorem set.nontrivial.iff_exists_lt

added theorem set.nontrivial.image

added theorem set.nontrivial.mono

added theorem set.nontrivial.ne_empty

added theorem set.nontrivial.ne_singleton

added theorem set.nontrivial.nonempty

added theorem set.nontrivial.not_subset_empty

added theorem set.nontrivial.not_subset_singleton

added theorem set.nontrivial.pair_subset

added theorem set.nontrivial.preimage

added theorem set.nontrivial_coe

added theorem set.nontrivial_iff_exists_ne

added theorem set.nontrivial_iff_pair_subset

modified theorem set.nontrivial_mono

added theorem set.nontrivial_of_exists_lt

added theorem set.nontrivial_of_exists_ne

added theorem set.nontrivial_of_image

added theorem set.nontrivial_of_lt

added theorem set.nontrivial_of_mem_mem_ne

added theorem set.nontrivial_of_nontrivial

added theorem set.nontrivial_of_nontrivial_coe

added theorem set.nontrivial_of_pair_subset

added theorem set.nontrivial_of_preimage

added theorem set.nontrivial_of_univ_nontrivial

added theorem set.nontrivial_pair

added theorem set.nontrivial_univ

added theorem set.nontrivial_univ_iff

added theorem set.not_nontrivial_empty

added theorem set.not_nontrivial_iff

added theorem set.not_nontrivial_singleton

added theorem set.not_subsingleton_iff