head!_le_of_lt

Mathlib.Topology.Category.Profinite.Nobeling.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.Products.head!_le_of_lt

← MathLib Explorer

English

If q < l and q.val ≠ [], then head! of q.val ≤ head! of l.val.

Русский

Если q < l и q.val ≠ [], то head!(q.val) ≤ head!(l.val).

LaTeX

$$$$ \\text{If } q < l \\text{ and } q.\\text{val} \\neq [] ,\\; q.\\text{val.head!} \\le l.\\text{val.head!}. $$$$

Lean4

theorem head!_le_of_lt [Inhabited I] {q l : Products I} (h : q < l) (hq : q.val ≠ []) : q.val.head! ≤ l.val.head! :=
  List.head!_le_of_lt l.val q.val h hq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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