Documentation
SpherePacking
.
ForMathlib
.
Cardinal
Search
return to top
source
Imports
Init
Mathlib.Data.Set.Card
Mathlib.SetTheory.Cardinal.Basic
Imported by
Cardinal
.
aux
source
theorem
Cardinal
.
aux
{
α
:
Type
u_1}
{
s
:
Set
α
}
:
toENat
(
mk
↑
s
)
=
s
.
encard