Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-09 13:36 ee018175

View on Github →

chore(data/set/basic): use decidable_pred (∈ s) instead of decidable_pred s. (#8211) The latter exploits the fact that sets are functions to Prop, and is an annoying form as lemmas are never stated about it. In future we should consider removing the set.decidable_mem instance which encourages this misuse. Making this change reveals a collection of pointless decidable arguments requiring that finset membership be decidable; something which is always true anyway. Two proofs in data/pequiv caused a crash inside the C++ portion of the finish tactic; it was easier to just write the simple proofs manually than to debug the C++ code.

Estimated changes

modified theorem equiv.set.insert_apply_left
modified def nat.subtype.of_nat
modified theorem pequiv.mem_of_set_iff
modified theorem pequiv.mem_of_set_self_iff
modified def pequiv.of_set
modified theorem pequiv.of_set_eq_refl
modified theorem pequiv.of_set_eq_some_iff
modified def pfun.eval_opt
modified def set.fintype_subset
modified theorem measurable.piecewise