Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 17:10 6a0f9674

View on Github →

feat(data/finite/set): finite instances for set constructions (#14673)

Estimated changes

Modified src/data/finite/basic.lean

Created src/data/finite/default.lean

Created src/data/finite/set.lean

added theorem finite.of_finite_univ

added theorem finite.set.finite_bUnion

added theorem finite.set.finite_of_finite_image

added theorem set.finite_iff_finite

added theorem set.finite_of_finite

added theorem set.finite_univ_iff