Documentation
LeanPool
.
PFR
.
Mathlib
.
Order
.
Interval
.
Finset
.
Fin
Search
return to top
source
Imports
Init
Mathlib.Order.Interval.Finset.Fin
Imported by
Fin
.
Iio_succ_eq_Iic_castSucc
Order intervals in
Fin
#
source
theorem
Fin
.
Iio_succ_eq_Iic_castSucc
{
n
:
ℕ
}
(
k
:
Fin
n
)
:
Finset.Iio
k
.
succ
=
Finset.Iic
k
.
castSucc