instMin_mathlib

Mathlib.Order.Fin.Basic

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

English

For every n and any a,b in Fin n, the value of the minimum matches the minimum of their values: (min a b).val = min(a.val, b.val).

Русский

Для любого n и любых a,b ∈ Fin n выполняется: (min a b).val = min(a.val, b.val).

LaTeX

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

Lean4

instance : Min (Fin n) where min x y := ⟨min x y, min_rec' (· < n) x.2 y.2⟩

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

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

Разделы

Аффилиация

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