Results on the cardinality of finitely supported functions and multisets. #
@[simp]
@[simp]
theorem
Cardinal.mk_finsupp_lift_of_infinite
(α : Type u)
(β : Type v)
[Infinite α]
[Zero β]
[Nontrivial β]
:
@[deprecated Cardinal.mk_eq_aleph0 (since := "2025-10-06")]
Alias of Cardinal.mk_eq_aleph0
.