Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv_of_subsingleton_of_subsingleton

Modification history

2020-05-30 04:46
src/data/equiv/basic.lean
feat(data/equiv): equiv_of_subsingleton_of_subsingleton (#2856)
Added equiv_of_subsingleton_of_subsingletonView on Github →