Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-05 06:25 dd8da516

View on Github →

refactor(*): migrate from ≠ ∅ to set.nonempty (#1954)

  • refactor(*): migrate from ≠ ∅ to set.nonempty Sorry for a huge PR but it's easier to do it in one go. Basically, I got rid of all ≠ ∅ in theorem/def types, then fixed compile. I also removed most lemmas about ≠ ∅ from set/basic to make sure that I didn't miss something I should change elsewhere. Should I restore (some of) them?
  • Fix compile of archive/
  • Drop +1 unneeded argument, thanks @sgouezel.

Estimated changes

modified theorem unique_diff_on_convex
modified theorem ennreal.coe_Inf
deleted theorem semiquot.ne_empty
added theorem semiquot.nonempty
added theorem set.empty_not_nonempty
modified theorem set.fst_image_prod
deleted theorem set.insert_ne_empty
modified theorem set.ne_empty_iff_nonempty
deleted theorem set.ne_empty_of_mem
modified theorem set.nmem_singleton_empty
modified theorem set.nonempty_compl
deleted theorem set.prod_ne_empty_iff
modified theorem set.range_eq_empty
deleted theorem set.range_ne_empty
added theorem set.range_nonempty
deleted theorem set.singleton_ne_empty
modified theorem set.snd_image_prod
deleted theorem set.subset_ne_empty
deleted theorem set.univ_ne_empty
modified theorem set.univ_nonempty
deleted theorem set.Ici_ne_empty
deleted theorem set.Iic_ne_empty
deleted theorem set.Iio_ne_empty
deleted theorem set.Ioi_ne_empty
deleted theorem ne_empty_of_is_glb
deleted theorem ne_empty_of_is_lub
added theorem nonempty_of_is_glb
added theorem nonempty_of_is_lub
modified theorem lattice.cInf_insert
modified theorem lattice.cInf_intro
modified theorem lattice.cInf_le_cInf
modified theorem lattice.cInf_le_cSup
modified theorem lattice.cInf_union
modified theorem lattice.cSup_insert
modified theorem lattice.cSup_inter_le
modified theorem lattice.cSup_intro'
modified theorem lattice.cSup_intro
modified theorem lattice.cSup_le
modified theorem lattice.cSup_le_cSup
modified theorem lattice.cSup_le_iff
modified theorem lattice.cSup_union
modified theorem lattice.cinfi_const
modified theorem lattice.cinfi_le
modified theorem lattice.cinfi_le_cinfi
modified theorem lattice.csupr_const
modified theorem lattice.csupr_le
modified theorem lattice.csupr_le_csupr
modified theorem lattice.is_glb_cInf
modified theorem lattice.is_lub_cSup
modified theorem lattice.le_cInf
modified theorem lattice.le_cInf_iff
modified theorem lattice.le_cInf_inter
modified theorem lattice.le_cinfi
modified theorem lattice.le_csupr
modified theorem with_top.coe_Inf
modified theorem filter.comap_ne_bot
modified theorem filter.nonempty_of_mem_sets
modified theorem filter.lift'_ne_bot_iff
modified theorem filter.Liminf_principal
modified theorem filter.Limsup_principal
modified theorem mem_closure_of_is_glb
modified theorem mem_closure_of_is_lub
modified theorem mem_of_is_glb_of_is_closed
modified theorem mem_of_is_lub_of_is_closed
modified theorem dense_iff_inter_open
modified theorem mem_closure_iff
modified theorem mem_closure_iff_nhds
modified theorem ennreal.Sup_add
modified theorem metric.diam_union'
modified theorem emetric.diam_union'
modified theorem metric.inf_edist_ne_top