zero_le'

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.zero_le'

English

For [NeZero n], every a in Fin n satisfies 0 ≤ a.

Русский

Для [NeZero n] любой a в Fin n имеет 0 ≤ a.

LaTeX

$$$\forall {n} (\text{[NeZero } n\text{]}), \forall a : Fin n, 0 \le a$$$

Lean4

@[deprecated Fin.zero_le (since := "2025-05-13")]
protected theorem zero_le' [NeZero n] (a : Fin n) : 0 ≤ a :=
  Nat.zero_le a.val

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

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

Разделы

Аффилиация

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