Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-01 16:37 15712902

View on Github →

feat(logic/is_empty): add some simp lemmas and unique instances (#7832) There are a handful of lemmas about (h : ¬nonempty a) that if restated in terms of [is_empty a] become suitable for simp or as instances. This adjusts some of those lemmas.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.eq_empty_of_is_empty

Modified src/data/matrix/basic.lean

modified theorem matrix.subsingleton_of_empty_left

modified theorem matrix.subsingleton_of_empty_right

Modified src/data/matrix/dmatrix.lean

modified theorem dmatrix.subsingleton_of_empty_left

modified theorem dmatrix.subsingleton_of_empty_right

Modified src/data/set/basic.lean

added theorem set.eq_empty_of_is_empty

added def set.unique_empty

Modified src/linear_algebra/char_poly/coeff.lean

Modified src/logic/embedding.lean

Modified src/logic/is_empty.lean

added theorem subtype.is_empty_of_false

Modified src/order/filter/basic.lean

added theorem filter.filter_eq_bot_of_is_empty

Modified src/set_theory/cardinal.lean

added theorem cardinal.eq_zero_of_is_empty

Modified src/set_theory/ordinal.lean