Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-24 05:22 2c84af16

View on Github →

feat(data/set/finite): unify fintype and finite developments Here fintype is the "constructive" one, which exhibits a list enumerating the set (quotiented over permutations), while "finite" merely states the existence of such a list.

Estimated changes

modified theorem is_open_sInter
added theorem finset.mem_univ_val
modified theorem list.nodup_filter_map
added theorem set.mem_def
modified theorem set.countable.to_encodable
modified theorem set.countable_encodable'
modified theorem set.countable_finite
added inductive set.finite'
added def set.finite
deleted inductive set.finite
added theorem set.finite_Union
added theorem set.finite_empty
modified theorem set.finite_image
modified theorem set.finite_insert
modified theorem set.finite_le_nat
modified theorem set.finite_prod
modified theorem set.finite_sUnion
modified theorem set.finite_singleton
modified theorem set.finite_subset
modified theorem set.finite_union
added theorem set.mem_to_finset
added theorem set.mem_to_finset_val
added def set.to_finset
added theorem set.sUnion_eq_Union'
deleted theorem function.partial_inv_eq