Structures · Data types
Countable
A type α is countable if there exists an injective map α → ℕ.
- Defined in
- Mathlib.Data.Countable.Defs
- Shape
- One type argument · adds exists_injective_nat'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Every Countable is also a
Provided automatically by
Concrete types that are instances51
- Int
- Nat
- Bool
- Quiver.Hom
- TopCat.carrier
- ENat
- FreeAbelianGroup
- Finsupp
- CategoryTheory.Discrete
- DFinsupp
- PNat
- FreeRing
- FreeCommRing
- FreeGroup
- FreeAddGroup
- FreeMonoid
- PProd
- PSum
- FreeAddMonoid
- FirstOrder.Language.Symbols
- List.Vector
- TopologicalSpace.Clopens
- IterateMulAct
- IterateAddAct
- FirstOrder.Language.Term
- DiscreteQuotient
- Nat.Primes
- FirstOrder.Language.Embedding
- FirstOrder.Language.Hom
- CategoryTheory.CountableCategory.ObjAsType
- CategoryTheory.CountableCategory.HomAsType
- FirstOrder.Language.Formula
- Subtype
- Prod
- Set.Elem
- ULift
- Fin
- PUnit
- WithTop
- WithBot
- Sum
- List
- Sigma
- Multiset
- Finset
- Option
- Quotient
- PLift
- Array
- Quot
- PSigma
How is a type an instance?
Loading the hierarchy index…
Assumed by657
- MeasurableSet.iUnion
- MeasureTheory.ae_all_iff
- Set.to_countable
- MeasureTheory.measure_iUnion_le
- MeasureTheory.measure_iUnion
- MeasurableSet.iInter
- ProbabilityTheory.Kernel.sum
- Set.countable_range
- Set.countable_iUnion
- Cardinal.mk_eq_aleph0
- MeasurableSet.univ_pi
- aemeasurable_pi_lambda
- Measurable.iSup
- nonempty_encodable
- MeasureTheory.measure_iUnion_null_iff
- MeasureTheory.lintegral_tsum
- exists_surjective_nat
- ProbabilityTheory.Kernel.sum.congr_simp
- Function.Injective.countable
- MeasureTheory.VectorMeasure.of_disjoint_iUnion
- Cardinal.mk_le_aleph0
- MeasureTheory.measure_iUnion₀
- MeasureTheory.NullMeasurableSet.iUnion
- Measurable.tsum
- eventually_countable_forall
- Encodable.ofCountable
- Set.countable_univ
- MeasureTheory.measure_iUnion_null
- TopologicalSpace.IsSeparable.iUnion
- MeasureTheory.Measure.prod_sum
- measurable_to_countable
- measurable_from_prod_countable_left
- ProbabilityTheory.Kernel.sum_zero
- MeasureTheory.Measure.toPMF
- ProbabilityTheory.Kernel.sum_apply'
- MeasureTheory.Egorov.iUnionNotConvergentSeq
- Measurable.iInf
- MeasureTheory.AEStronglyMeasurable.of_discrete
- IsGδ.iInter_of_isOpen
- aeSeq.measure_compl_aeSeqSet_eq_zero
- ProbabilityTheory.setBernoulli_ae_subset
- BoxIntegral.Box.measurableSet_coe
- Directed.measure_iUnion
- ENNReal.exists_pos_sum_of_countable'
- MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume
- MeasureTheory.Measure.restrict_iUnion_ae
- MeasureTheory.lintegral_iUnion
- Countable.exists_injective_nat
- MeasureTheory.Adapted.isStoppingTime_hittingBtwn
- MeasureTheory.Measure.restrict_iUnion_le