instMax_mathlib

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.instMax_mathlib

English

For every n and any a,b in Fin n, the value of the maximum coincides with the maximum of their values: (max a b).val = max(a.val, b.val).

Русский

Для любого n и для любых a,b ∈ Fin n верно: (max a b).val = max(a.val, b.val).

LaTeX

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

Lean4

instance : Max (Fin n) where max x y := ⟨max x y, max_rec' (· < n) x.2 y.2⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru