finToNat — Mathlib

English

A Fin(n)-graded order on α is also a Nat-graded order on α.

Русский

Упорядочение α с градацией Fin(n) также можно рассматривать как Nat-градиент на α.

LaTeX

$$$[GradeOrder (Fin n) α] \\Rightarrow [GradeOrder \\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 : ℕ) [GradeOrder (Fin n) α] : GradeOrder ℕ α :=
  (GradeOrder.liftLeft (_ : Fin n → ℕ) Fin.val_strictMono) fun _ _ => CovBy.coe_fin

Похожие утверждения