Commit 2022-11-11 01:58 ed092fc2

View on Github →

feat: port Mathlib.Logic.Nontrivial (#547) The simp tag is registered in a separate file

Estimated changes

Modified Mathlib/Logic/Nontrivial.lean

added theorem Pi.nontrivial_at

added theorem Subtype.nontrivial_iff_exists_ne

added theorem exists_ne

added theorem exists_pair_lt

added theorem exists_pair_ne

added theorem false_of_nontrivial_of_subsingleton

added theorem nontrivial_iff

added theorem nontrivial_iff_exists_ne

added theorem nontrivial_iff_lt

added theorem nontrivial_of_lt

added theorem nontrivial_of_ne

added theorem not_nontrivial

added theorem not_nontrivial_iff_subsingleton

added theorem not_subsingleton

added theorem subsingleton_iff

added theorem subsingleton_or_nontrivial