Documentation
FormalConjecturesForMathlib
.
Order
.
Interval
.
Finset
.
Nat
Search
return to top
source
Imports
Init
Mathlib.Data.Set.Card
Mathlib.Order.Interval.Finset.Nat
Imported by
Nat
.
ncard_Iio
source
@[simp]
theorem
Nat
.
ncard_Iio
(
b
:
ℕ
)
:
(
Set.Iio
b
)
.
ncard
=
b