Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 06:40 4dee658e

View on Github →

chore(set_theory/zfc): general cleanup (#15208) This PR does the following:

  • Make pSet.mk_type_func into a simp lemma, rename to pSet.eta.
  • Give a simpler definition for pSet.empty.
  • Enable dot notation on resp.equiv and separate the symm and trans theorems from the setoid instance.
  • Protect lemmas to avoid trouble between the equiv and the resp.equiv lemmas.
  • Tweak some spacing.
  • Add many missing simp tags.

Estimated changes

modified theorem Set.mk_eq
modified theorem Set.subset_iff
deleted theorem pSet.equiv.euc
deleted theorem pSet.equiv.refl
deleted theorem pSet.equiv.rfl
deleted theorem pSet.equiv.symm
deleted theorem pSet.equiv.trans
added theorem pSet.eta
modified theorem pSet.mem.mk
modified theorem pSet.mem_Union
modified theorem pSet.mem_empty
modified theorem pSet.mem_powerset
deleted theorem pSet.mk_type_func
deleted theorem pSet.resp.euc
deleted theorem pSet.resp.refl