Embeddings of Fin n
#
Fin n
is the type whose elements are natural numbers smaller than n
.
This file defines embeddings between Fin n
and other types,
Main definitions #
Fin.valEmbedding
: coercion to natural numbers as anEmbedding
;Fin.succEmb
:Fin.succ
as anEmbedding
;Fin.castLEEmb h
:Fin.castLE
as anEmbedding
, embedFin n
intoFin m
,h : n ≤ m
;finCongr
:Fin.cast
as anEquiv
, equivalence betweenFin n
andFin m
whenn = m
;Fin.castAddEmb m
:Fin.castAdd
as anEmbedding
, embedFin n
intoFin (n+m)
;Fin.castSuccEmb
:Fin.castSucc
as anEmbedding
, embedFin n
intoFin (n+1)
;Fin.addNatEmb m i
:Fin.addNat
as anEmbedding
, addm
oni
on the right, generalizesFin.succ
;Fin.natAddEmb n i
:Fin.natAdd
as anEmbedding
, addsn
oni
on the left;
order #
@[simp]
succ and casts into larger Fin types #
@[deprecated Fin.coe_succEmb (since := "2025-04-12")]
Alias of Fin.coe_succEmb
.
Fin.castLE
as an Embedding
, castLEEmb h i
embeds i
into a larger Fin
type.
Equations
- Fin.castLEEmb h = { toFun := Fin.castLE h, inj' := ⋯ }
Instances For
Fin.castAdd
as an Embedding
, castAddEmb m i
embeds i : Fin n
in Fin (n+m)
.
See also Fin.natAddEmb
and Fin.addNatEmb
.
Equations
Instances For
Fin.natAdd
as an Embedding
, natAddEmb n i
adds n
to i
"on the left".
Equations
- Fin.natAddEmb n = { toFun := Fin.natAdd n, inj' := ⋯ }
Instances For
Fin.succAbove p
as an Embedding
.
Equations
- p.succAboveEmb = { toFun := p.succAbove, inj' := ⋯ }
Instances For
@[simp]