coe_max — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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