# Results on the cardinality of finitely supported functions and multisets. #

source
@[simp]
theorem Cardinal.mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [Fintype α] [Zero β] :
mk (α →₀ β) = lift.{u, v} (mk β) ^ Fintype.card α
source
theorem Cardinal.mk_finsupp_of_fintype (α β : Type u) [Fintype α] [Zero β] :
mk (α →₀ β) = mk β ^ Fintype.card α
source
@[simp]
theorem Cardinal.mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] :
mk (α →₀ β) = max (lift.{v, u} (mk α)) (lift.{u, v} (mk β))
source
theorem Cardinal.mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] :
mk (α →₀ β) = max (mk α) (mk β)
source
@[simp]
theorem Cardinal.mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] :
mk (α →₀ β) = max (lift.{v, u} (mk α)) (lift.{u, v} (mk β))
source
theorem Cardinal.mk_finsupp_of_infinite' (α β : Type u) [Nonempty α] [Zero β] [Infinite β] :
mk (α →₀ β) = max (mk α) (mk β)
source
theorem Cardinal.mk_finsupp_nat (α : Type u) [Nonempty α] :
mk (α →₀ ℕ) = max (mk α) aleph0
source
theorem Cardinal.mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] :
mk (Multiset α) = 1
source
@[simp]
theorem Cardinal.mk_multiset_of_nonempty (α : Type u) [Nonempty α] :
mk (Multiset α) = max (mk α) aleph0
source
theorem Cardinal.mk_multiset_of_infinite (α : Type u) [Infinite α] :
mk (Multiset α) = mk α
source
@[deprecated Cardinal.mk_eq_aleph0 (since := "2025-10-06")]
theorem Cardinal.mk_multiset_of_countable (α : Type u_1) [Countable α] [Infinite α] :
mk α = aleph0

Alias of `Cardinal.mk_eq_aleph0`.