Documentation
Mathlib
.
Data
.
Fin
.
EquivOfInjective
Search
return to top
source
Imports
Init
Mathlib.Data.Fin.SuccPred
Mathlib.Logic.Equiv.Set
Imported by
Fin
.
coe_of_injective_castLE_symm
Fin
.
coe_of_injective_castSucc_symm
source
@[deprecated Equiv.apply_ofInjective_symm (since := "2026-08-26")]
theorem
Fin
.
coe_of_injective_castLE_symm
{
n
k
:
ℕ
}
(
h
:
n
≤
k
)
(
i
:
Fin
k
)
(
hi
:
i
∈
Set.range
(
castLE
h
)
)
:
↑
(
(
Equiv.ofInjective
(
castLE
h
)
⋯
)
.
symm
⟨
i
,
hi
⟩
)
=
↑
i
source
@[deprecated Equiv.apply_ofInjective_symm (since := "2026-08-26")]
theorem
Fin
.
coe_of_injective_castSucc_symm
{
n
:
ℕ
}
(
i
:
Fin
n
.
succ
)
(
hi
:
i
∈
Set.range
castSucc
)
:
↑
(
(
Equiv.ofInjective
castSucc
⋯
)
.
symm
⟨
i
,
hi
⟩
)
=
↑
i