Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-12 09:04 bd59f822

View on Github →

feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901) Also make the argument to set.finite_or_infinite explicit.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.eq_singleton_or_nontrivial

Modified src/data/set/basic.lean

added theorem set.eq_singleton_or_nontrivial

Modified src/data/set/finite.lean

deleted theorem set.finite_or_infinite

Modified src/order/well_founded_set.lean