Structures · Data types
Uncountable
A type α is uncountable if it is not countable.
- Defined in
- Mathlib.Data.Countable.Defs
- Shape
- One type argument · adds not_countable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Uncountable is also a
Concrete types that are instances11
- Real
- Ordinal
- Cardinal
- Prod
- ULift
- WithTop
- WithBot
- Sum
- Sigma
- Option
- PLift
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- Function.Injective.uncountable
- not_countable
- Set.not_countable_univ
- Uncountable.not_countable
- Uncountable.of_equiv
- instUncountableULift
- Sum.uncountable_inr
- instUncountableSigmaOfNonempty
- Cardinal.exists_uncountable_fiber
- Function.Surjective.uncountable
- instInfiniteOfUncountable
- Option.instUncountable
- WithTop.instUncountable
- instUncountablePLift
- Function.Embedding.uncountable
- Cardinal.aleph0_lt_mk
- instUncountableProdOfNonempty_1
- instUncountableProdOfNonempty
- not_surjective_countable_uncountable
- WithBot.instUncountable
- Cardinal.aleph1_le_mk
- Finsupp.Uncountable.of_moduleFinite
- not_injective_uncountable_countable
- Sum.uncountable_inl
- Sigma.uncountable