Structures · Lean core

Subsingleton

A _subsingleton_ is a type with at most one element. It is either empty or has a unique element. All propositions are subsingletons because of proof irrelevance: false propositions are empty, and all proofs of a true proposition are equal to one another. Some non-propositional types are also subsingletons.

Defined in: Init.Core
Shape: One type argument · adds allEq

Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Every Subsingleton is also a

Provided automatically by

Concrete types that are instances100

Quiver.Hom
SeparationQuotient
CategoryTheory.Functor.obj
BitVec
CStarMatrix
CommRingCat.carrier
RatFunc
Quaternion
Matrix
HahnSeries
NonemptyInterval
LocallyConstant
QuadraticAlgebra
Units
Finsupp
UniformFun
UniformOnFun
CategoryTheory.Discrete
SymAlg
Localization
AddUnits
LocalizedModule
QuaternionAlgebra
TopologicalSpace.NonemptyCompacts
Empty
Matrix.SpecialLinearGroup
FundamentalGroupoid
Representation.IntertwiningMap
PEmpty
AlgEquiv
LieSubalgebra
LieSubmodule
MeasureTheory.Measure
MeasureTheory.VectorMeasure
AddMonoidHom
ArchimedeanClass
OneHom
DMatrix
ZeroHom
Sym2
ClassGroup
ProbabilityTheory.Kernel
SSet.Truncated.HomotopyCategory
NonUnitalSubalgebra
NonUnitalStarSubalgebra
KaehlerDifferential
CommRing.Pic
Algebra.Extension.H1Cotangent
AlgebraicGeometry.Scheme.EllAdicCohomology
AlgHom
BooleanSubalgebra
PrincipalSeg
Sym
LieIdeal
WithTopology
SimpleGraph.ConnectedComponent
RingCon
BialgHom
PowerSeries
FirstOrder.Language.Relations
SuccOrder
PredOrder
SimpleGraph.Hom
OnePoint
NonUnitalStarAlgHom
Path
List.Vector
MonoidWithZeroHom
CoalgHom
MulArchimedeanClass
OrderRingHom
RingEquiv
Antisymmetrization
MulArchimedeanOrder
OrderIso
ArchimedeanOrder
NonUnitalAlgHom
NumberField.InfinitePlace
ConnectedComponents
InitialSeg
ZerothHomotopy
CategoryTheory.Iso
CategoryTheory.ShortComplex.HomologyMapData
Decidable
CategoryTheory.Functor.WellOrderInductionData.Extension
CategoryTheory.ShortComplex.RightHomologyMapData
CategoryTheory.ShortComplex.LeftHomologyMapData
OrderRingIso
PresheafOfModules.Sheafify.SMulCandidate
SimpleGraph.EdgeLabeling
StateM
DirichletCharacter
SimpleGraph.Copy
LinearMap.BilinForm.Isometry
MeasureTheory.NullMeasurableSpace
QuadraticMap.Isometry
WeierstrassCurve.Affine.CoordinateRing
SSet.Truncated.Edge
PFunctor.Approx.CofixA
CategoryTheory.Limits.colimit

How is a type an instance?

Loading the hierarchy index…