Documentation

Mathlib.SetTheory.Cardinal.Finsupp

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

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