Fin n
forms a bounded linear order #
This file contains the linear ordered instance on Fin n
.
Fin n
is the type whose elements are natural numbers smaller than n
.
This file expands on the development in the core library.
Main definitions #
Fin.orderIsoSubtype
: coercion to{i // i < n}
as anOrderIso
;Fin.valEmbedding
: coercion to natural numbers as anEmbedding
;Fin.valOrderEmb
: coercion to natural numbers as anOrderEmbedding
;Fin.succOrderEmb
:Fin.succ
as anOrderEmbedding
;Fin.castLEOrderEmb h
:Fin.castLE
as anOrderEmbedding
, embedFin n
intoFin m
whenh : n ≤ m
;Fin.castOrderIso
:Fin.cast
as anOrderIso
, order isomorphism betweenFin n
andFin m
provided thatn = m
, see alsoEquiv.finCongr
;Fin.castAddOrderEmb m
:Fin.castAdd
as anOrderEmbedding
, embedFin n
intoFin (n+m)
;Fin.castSuccOrderEmb
:Fin.castSucc
as anOrderEmbedding
, embedFin n
intoFin (n+1)
;Fin.addNatOrderEmb m i
:Fin.addNat
as anOrderEmbedding
, addm
oni
on the right, generalizesFin.succ
;Fin.natAddOrderEmb n i
:Fin.natAdd
as anOrderEmbedding
, addsn
oni
on the left;Fin.revOrderIso
:Fin.rev
as anOrderIso
, the antitone involution given byi ↦ n-(i+1)
Instances #
Equations
Equations
Extra instances to short-circuit type class resolution #
These also prevent non-computable instances being used to construct these instances non-computably.
Equations
Miscellaneous lemmas #
Monotonicity #
Fin.predAbove p
as an OrderHom
.
Equations
- p.predAboveOrderHom = { toFun := p.predAbove, monotone' := ⋯ }
Order isomorphisms #
The equivalence Fin n ≃ {i // i < n}
is an order isomorphism.
Equations
castOrderIso eq i
embeds i
into an equal Fin
type.
Equations
- Fin.castOrderIso eq = { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
While in many cases Fin.castOrderIso
is better than Equiv.cast
/cast
, sometimes we want to
apply a generic lemma about cast
.
Fin.rev n
as an order-reversing isomorphism.
Equations
- Fin.revOrderIso = { toEquiv := OrderDual.ofDual.trans Fin.revPerm, map_rel_iff' := ⋯ }
Order embeddings #
The inclusion map Fin n → ℕ
is an order embedding.
Equations
- Fin.valOrderEmb n = { toEmbedding := Fin.valEmbedding, map_rel_iff' := ⋯ }
The ordering on Fin n
is a well order.
Fin.succ
as an OrderEmbedding
Equations
Fin.castAdd
as an OrderEmbedding
.
castAddEmb m i
embeds i : Fin n
in Fin (n+m)
. See also Fin.natAddEmb
and Fin.addNatEmb
.
Equations
Fin.castSucc
as an OrderEmbedding
.
castSuccOrderEmb i
embeds i : Fin n
in Fin (n+1)
.
Fin.addNat
as an OrderEmbedding
.
addNatOrderEmb m i
adds m
to i
, generalizes Fin.succ
.
Equations
- Fin.addNatOrderEmb m = OrderEmbedding.ofStrictMono (fun (x : Fin n) => x.addNat m) ⋯
Fin.succAbove p
as an OrderEmbedding
.
Equations
Uniqueness of order isomorphisms #
Two strictly monotone functions from Fin n
are equal provided that their ranges
are equal.