head_le

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#LTSeries.head_le

English

For every x: LTSeries α and every n in Fin (x.length + 1), the head is ≤ x(n).

Русский

Для каждого x: LTSeries α и любого n ∈ Fin(x.length + 1) выполняется head ≤ x(n).

LaTeX

$$$\forall {\alpha}\ [Preorder\alpha] (x: LTSeries\alpha) (n: Fin (x.length + 1)), x.head \le x n$$$

Lean4

theorem head_le (x : LTSeries α) (n : Fin (x.length + 1)) : x.head ≤ x n :=
  x.monotone (Fin.zero_le n)

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

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

Разделы

Аффилиация

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