Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-14 21:29 79483182

View on Github →

feat(logic/basic): add rewrite rules for nonempty

Estimated changes

added theorem classical.nonempty_pi
added theorem nonempty.exists
added theorem nonempty.forall
added theorem nonempty_Prop
added theorem nonempty_empty
added theorem nonempty_plift
added theorem nonempty_pprod
added theorem nonempty_prod
added theorem nonempty_psigma
added theorem nonempty_psum
added theorem nonempty_sigma
added theorem nonempty_subtype
added theorem nonempty_sum
added theorem nonempty_ulift