coe_min — Mathlib

English

The natural-number representation of the minimum on Fin n equals the minimum of the representations: ↑(min a b) = min(a.val, b.val).

Русский

Естественная вложенная в ℕ величина минимума на Fin n равна минимуму значений: ↑(min a b) = min(a.val, b.val).

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_min (a b : Fin n) : ↑(min a b) = (min a b : ℕ) :=
  rfl

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