Commit 2022-10-25 00:59 2f2b44ae

View on Github →

feat: Port Logic.Nonempty (#487)

  • Deleted nonempty_empty since std4 now has that as not_nonempty_empty and as a simp lemma
  • Added an import to access Zero for Zero.Nonempty
  • Could not provide a One.Nonempty because One isn't defined yet
  • Used mathport's implicit type params, not sure what the style guidelines are
  • Gave previously anonymous instances names: Prod.Nonempty, Pi.Nonempty

Estimated changes

modified theorem Classical.nonempty_pi
modified theorem Nonempty.elim_to_inhabited
modified theorem Nonempty.exists
modified theorem Nonempty.forall
modified theorem Nonempty.map
modified theorem exists_true_iff_nonempty
modified theorem nonempty_Prop
modified theorem nonempty_plift
modified theorem nonempty_pprod
modified theorem nonempty_psigma
modified theorem nonempty_psum
modified theorem nonempty_sigma
modified theorem nonempty_subtype
modified theorem not_nonempty_iff_imp_false