Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-06 22:53 117e93f8

View on Github →

feat(data/set/finite): Align set.to_finset and set.finite.to_finset (#17959) Match lemmas about set.to_finset and set.finite.to_finset. This mostly involves making sure we have all pairs of the form set.to_finset_whatever/set.finite.to_finset_whatever. Also add a few lemmas and tag existing ones with simp.

Estimated changes

added theorem finset.mem_val
added theorem set.disjoint_to_finset
deleted theorem set.mem_to_finset_val
added theorem set.ssubset_to_finset
added theorem set.subset_to_finset
modified theorem set.to_finset_compl
modified theorem set.to_finset_diff
modified theorem set.to_finset_empty
added theorem set.to_finset_eq_empty
modified theorem set.to_finset_eq_univ
added theorem set.to_finset_image
modified theorem set.to_finset_inter
deleted theorem set.to_finset_ne_eq_erase
added theorem set.to_finset_set_of
modified theorem set.to_finset_ssubset
modified theorem set.to_finset_subset
modified theorem set.to_finset_union
modified theorem set.to_finset_univ
deleted theorem set.finite.coe_to_finset
deleted theorem set.finite.mem_to_finset
deleted theorem set.finite.to_finset_inj
modified theorem set.finite.to_finset_subset
deleted theorem set.finite_univ_to_finset
deleted theorem set.subset_to_finset_iff