Documentation
Std
.
Data
.
Fin
.
Lemmas
Search
Google site search
return to top
source
Imports
Init
Std.Data.Fin.Basic
Imported by
Fin
.
coe_clamp
clamp
#
source
@[simp]
theorem
Fin
.
coe_clamp
(n :
Nat
)
(m :
Nat
)
:
↑
(
Fin.clamp
n
m
)
=
min
n
m