Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 19:58 a0b6bab2

View on Github →

split(logic/nonempty): Split off logic.basic (#10762) This moves the lemmas about nonempty to a new file logic.basic I'm crediting Johannes for 79483182abffcac3a1ddd7098d47a475e75a5ed2

Estimated changes

deleted theorem classical.nonempty_pi
deleted theorem exists_true_iff_nonempty
deleted theorem nonempty.exists
deleted theorem nonempty.forall
deleted theorem nonempty.map
deleted theorem nonempty_Prop
deleted theorem nonempty_empty
deleted theorem nonempty_plift
deleted theorem nonempty_pprod
deleted theorem nonempty_prod
deleted theorem nonempty_psigma
deleted theorem nonempty_psum
deleted theorem nonempty_sigma
deleted theorem nonempty_subtype
deleted theorem nonempty_sum
deleted theorem nonempty_ulift
added theorem classical.nonempty_pi
added theorem nonempty.exists
added theorem nonempty.forall
added theorem nonempty.map
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