English
A Fin(n)-graded order on α is Nat-graded with minimality transported from Fin(n) to Nat.
Русский
Упорядочение α с градацией Fin(n) имеет Nat-градицию, где минимальные элементы соответствуют исходному Fin(n).
LaTeX
$$$[GradeMinOrder (Fin n) α] \\Rightarrow [GradeMinOrder \\mathbb{N} α]$$$
Lean4
/-- A `Fin n`-graded order is also `ℕ`-graded. We do not mark this an instance because `n` is not
inferable. -/
abbrev finToNat (n : ℕ) [GradeMinOrder (Fin n) α] : GradeMinOrder ℕ α :=
(GradeMinOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono fun _ _ => CovBy.coe_fin) fun a h =>
by
cases n
· exact a.elim0
rw [h.eq_bot, Fin.bot_eq_zero]
exact isMin_bot
