basic): unique and fintype of subtype of one element (#8491)

Commit

4 years ago

feat(logic/unique,data/fintype/basic): unique and fintype of subtype of one element (#8491) Additionally, a lemma proving that the cardinality of such a subtype is 1.

Author

pechersky

Parents

eb73c357

mathlib3 c2a0532f - feat(logic/unique,data/fintype/basic): unique and fintype of subtype of one element (#8491)

mathlib3
c2a0532f - feat(logic/unique,data/fintype/basic): unique and fintype of subtype of one element (#8491)