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 (α →₀ β) = lift.{v, u} (mk α) ⊔ lift.{u, v} (mk β)

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

@[simp]

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

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

theorem Cardinal.mk_finsupp_nat (α : Type u) [Nonempty α] : mk (α →₀ ℕ) = 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 α) = mk α ⊔ aleph0

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

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