Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subsingleton_of_univ_subsingleton

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_of_univ_subsingleton View on Github →