Mathlib v3 is deprecated. Go to Mathlib v4

Inductive set.finite

Modification history

2022-06-02 17:31
src/data/set/finite.lean
refactor(data/set/finite): protect `set.finite` (#14344) …
Modified set.finiteView on Github →
2021-09-15 18:42
src/data/set/finite.lean
refactor(data/set/finite): use a custom inductive type (#9164) …
Added set.finiteView on Github →
2017-11-24 05:22
data/set/finite.lean
feat(data/set/finite): unify fintype and finite developments …
Deleted set.finiteView on Github →
2017-07-23 15:16
data/set/finite.lean
refactor(*): import content from lean/library/data and library_dev
Added set.finiteView on Github →