Results on the cardinality of finitely supported functions and multisets.

@[simp]

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

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

@[simp]

theorem Cardinal.mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] : Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))

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

@[simp]

theorem Cardinal.mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [Nonempty α] [Zero β] [Infinite β] : Cardinal.mk (α →₀ β) = max (Cardinal.lift.{v, u} (Cardinal.mk α)) (Cardinal.lift.{u, v} (Cardinal.mk β))

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

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

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

@[simp]

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

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

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