Structures · Data types
Infinite
A type is said to be infinite if it is not finite. Note that Infinite α is equivalent to
IsEmpty (Fintype α) or IsEmpty (Finite α).
- Defined in
- Mathlib.Data.Finite.Defs
- Shape
- One type argument · adds not_finite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Every Infinite is also a
Provided automatically by
Concrete types that are instances41
- Int
- Nat
- ZMod
- Polynomial
- FreeAbelianGroup
- Finsupp
- DFinsupp
- FreeRing
- FreeCommRing
- FreeGroup
- FreeAddGroup
- Equiv.Perm
- Sym2
- String
- MvPolynomial
- Sym
- FreeMonoid
- WithTopology
- FreeAddMonoid
- OnePoint
- DihedralGroup
- UpperHalfPlane
- Field.Emb
- SimpleGraph.Coloring
- Nat.Primes
- EuclideanSpace
- Subtype
- Prod
- Set.Elem
- ULift
- HasQuotient.Quotient
- Sum
- Multiplicative
- List
- Additive
- Sigma
- Set
- Multiset
- Finset
- Option
- PLift
How is a type an instance?
Loading the hierarchy index…
Assumed by271
- Nat.card_eq_zero_of_infinite
- Cardinal.aleph0_le_mk
- Filter.hyperfilter
- Cardinal.mk_eq_aleph0
- Set.infinite_univ
- Infinite.natEmbedding
- intEquivOfZPowersEqTop
- ENat.card_eq_top_of_infinite
- Infinite.of_injective
- not_finite
- Set.infinite_range_of_injective
- ClassGroup.finsetApprox
- Nat.Subtype.ofNat
- not_injective_infinite_finite
- Cardinal.mk_finsupp_lift_of_infinite'
- Set.Finite.exists_lt_map_eq_of_forall_mem
- Cardinal.mk_finsupp_lift_of_infinite
- Nat.Subtype.succ
- Nat.orderEmbeddingOfSet
- Fintype.false
- MvPolynomial.funext
- Infinite.exists_subset_card_eq
- Infinite.not_finite
- Finite.exists_ne_map_eq_of_infinite
- AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite
- ClassGroup.distinctElems
- Nat.Subtype.orderIsoOfNat
- intEquivOfZMultiplesEqTop
- ENNReal.tsum_const_eq_top_of_ne_zero
- Cardinal.mk_list_eq_mk
- Infinite.exists_superset_card_eq
- Finite.false
- MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite
- Nat.Subtype.exists_succ
- Cardinal.add_mk_eq_max
- Cardinal.mk_compl_of_infinite
- Denumerable.ofEncodableOfInfinite
- Set.infinite_iUnion
- Infinite.exists_notMem_finset
- Cardinal.mk_finset_of_infinite
- Module.Free.infinite
- zpowersHom_bijective
- LinearMap.exists_isNilRegular
- intEquivOfZPowersEqTop_apply
- ClassGroup.prod_finsetApprox_ne_zero
- infinite_basis_le_maximal_linearIndependent'
- Set.infinite_of_finite_compl
- Cardinal.mk_perm_eq_self_power
- Filter.map_card_atTop
- Polynomial.funext