Results on the cardinality of finitely supported functions and multisets.

@[simp]

theorem Cardinal.mk_finsupp_lift_of_fintype (α : Type u) (β : Type v) [Fintype α] [Zero β] : mk (α →₀ β) = lift.{u, v} (mk β) ^ Fintype.card α

theorem Cardinal.mk_finsupp_of_fintype (α β : Type u) [Fintype α] [Zero β] : mk (α →₀ β) = mk β ^ Fintype.card α

@[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 β))

theorem Cardinal.mk_finsupp_of_infinite (α β : Type u) [Infinite α] [Zero β] [Nontrivial β] : mk (α →₀ β) = max (mk α) (mk β)

@[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 β))

theorem Cardinal.mk_finsupp_of_infinite' (α β : Type u) [Nonempty α] [Zero β] [Infinite β] : mk (α →₀ β) = max (mk α) (mk β)

theorem Cardinal.mk_finsupp_nat (α : Type u) [Nonempty α] : mk (α →₀ ℕ) = max (mk α) aleph0

theorem Cardinal.mk_multiset_of_isEmpty (α : Type u) [IsEmpty α] : mk (Multiset α) = 1

@[simp]

theorem Cardinal.mk_multiset_of_nonempty (α : Type u) [Nonempty α] : mk (Multiset α) = max (mk α) aleph0

theorem Cardinal.mk_multiset_of_infinite (α : Type u) [Infinite α] : mk (Multiset α) = mk α

@[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.