Commit 2024-10-12 06:38 21dee83e

View on Github →

chore(*): assume [Nonempty α] [Subsingleton α] instead of Unique α (#17670)

Estimated changes

Modified Mathlib/Analysis/Convex/Basic.lean

modified theorem stdSimplex_unique

Modified Mathlib/Logic/Unique.lean

added theorem nonempty_unique

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.mk_eq_one

Modified Mathlib/SetTheory/Cardinal/Finite.lean

modified theorem Nat.card_unique

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Ordinal.type_eq_one_of_unique

Modified Mathlib/Topology/Homotopy/Contractible.lean

Modified Mathlib/Topology/TietzeExtension.lean