compare_eq_compare_val — Mathlib

English

The comparison on Fin n is determined by the comparison of underlying values: compare a b = compare a.val b.val.

Русский

Сравнение на Fin n определяется сравнением базовых значений: compare a b = compare a.val b.val.

LaTeX

$$$\forall {n : \mathbb{N}} \, (a,b : \mathrm{Fin}\,n),\ \mathrm{compare}\, a\, b = \mathrm{compare}\, a.val\, b.val$$$

Lean4

theorem compare_eq_compare_val (a b : Fin n) : compare a b = compare a.val b.val :=
  rfl

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