Documentation
PFR
.
Mathlib
.
Order
.
Interval
.
Finset
.
Fin
Search
return to top
source
Imports
Init
Mathlib.Order.Interval.Finset.Fin
Imported by
Iio_of_succ_eq_Iic_of_castSucc
source
theorem
Iio_of_succ_eq_Iic_of_castSucc
{
N
:
ℕ
}
(
n
:
Fin
N
)
:
Finset.Iio
n
.
succ
=
Finset.Iic
n
.
castSucc