Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subsingleton_univ_iff

Modification history

2021-10-06 06:05
src/data/set/basic.lean
feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are 1 in zero dimensions (#9564)
Added set.subsingleton_univ_iffView on Github →