Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-30 13:27 b4b05dd2

View on Github →

feat(logic/basic): introduce pempty

Estimated changes

Modified data/equiv/basic.lean

deleted def equiv.arrow_empty_unit

added def equiv.equiv_pempty

added def equiv.false_equiv_pempty

added def equiv.pempty_arrow_equiv_unit

added def equiv.pempty_equiv_pempty

added def equiv.pempty_prod

added def equiv.pempty_sum

added def equiv.prod_pempty

added def equiv.sum_pempty

Modified data/fintype.lean

added theorem fintype.card_pempty

added theorem fintype.univ_pempty

Modified logic/basic.lean

added def pempty.elim

added inductive {u}

Modified set_theory/cardinal.lean

Modified tactic/auto_cases.lean