Finite order homomorphisms. #
The fundamental order homomorphisms between Fin (n + 1)
and Fin n
.
Fin.succAbove p i
:succAbove p i
embedsFin n
intoFin (n + 1)
with a hole aroundp
.Fin.succAboveEmb p
:Fin.succAbove p
as anOrderEmbedding
.Fin.predAbove p i
: surjectsi : Fin (n+1)
intoFin n
by subtracting one ifp < i
.
@[simp]
Fin.succAbove p
as an OrderEmbedding
.
Equations
- p.succAboveEmb = OrderEmbedding.ofStrictMono p.succAbove ⋯
Instances For
@[deprecated Fin.castSucc_lt_or_lt_succ]
Alias of Fin.castSucc_lt_or_lt_succ
.
succAbove
is injective at the pivot
@[simp]
theorem
Fin.succ_succAbove_one
{n : ℕ}
[NeZero n]
(i : Fin (n + 1))
:
i.succ.succAbove 1 = (i.succAbove 0).succ
By moving succ
to the outside of this expression, we create opportunities for further
simplification using succAbove_zero
or succ_succAbove_zero
.
@[simp]
@[simp]
@[simp]
theorem
Fin.succ_predAbove_zero
{n : ℕ}
[NeZero n]
{j : Fin (n + 1)}
(h : j ≠ 0)
:
(Fin.predAbove 0 j).succ = j
@[simp]
theorem
Fin.predAbove_zero_of_ne_zero
{n : ℕ}
[NeZero n]
{i : Fin (n + 1)}
(hi : i ≠ 0)
:
Fin.predAbove 0 i = i.pred hi
theorem
Fin.predAbove_zero
{n : ℕ}
[NeZero n]
{i : Fin (n + 1)}
:
Fin.predAbove 0 i = if hi : i = 0 then 0 else i.pred hi