Commit 2024-04-18 05:39 493a947e

View on Github →

chore: split Subsingleton,Nontrivial off of Data.Set.Basic (#11832) Moves definition of and lemmas related to Set.Subsingleton and Set.Nontrivial to a new file, so that Basic can be shorter.

Estimated changes

deleted theorem Set.Nontrivial.exists_lt
deleted theorem Set.Nontrivial.exists_ne
deleted theorem Set.Nontrivial.mono
deleted theorem Set.Subsingleton.anti
deleted theorem Set.Subsingleton.coe_sort
deleted theorem Set.antitoneOn_singleton
deleted theorem Set.monotoneOn_singleton
deleted theorem Set.nontrivial_coe_sort
deleted theorem Set.nontrivial_mono
deleted theorem Set.nontrivial_of_lt
deleted theorem Set.nontrivial_pair
deleted theorem Set.nontrivial_univ
deleted theorem Set.nontrivial_univ_iff
deleted theorem Set.not_nontrivial_empty
deleted theorem Set.not_nontrivial_iff
deleted theorem Set.not_subsingleton_iff
deleted theorem Set.subsingleton_coe
deleted theorem Set.subsingleton_empty
deleted theorem Set.subsingleton_isBot
deleted theorem Set.subsingleton_isTop
deleted theorem Set.subsingleton_univ
deleted theorem Set.subsingleton_univ_iff
deleted theorem Set.univ_eq_true_false
added theorem Set.Nontrivial.mono
added theorem Set.Subsingleton.anti
added theorem Set.nontrivial_mono
added theorem Set.nontrivial_of_lt
added theorem Set.nontrivial_pair
added theorem Set.nontrivial_univ
added theorem Set.not_nontrivial_iff
added theorem Set.subsingleton_coe
added theorem Set.subsingleton_empty
added theorem Set.subsingleton_isBot
added theorem Set.subsingleton_isTop
added theorem Set.subsingleton_univ
added theorem Set.univ_eq_true_false