shortlex_def

Mathlib.Data.List.Shortlex

URI: https://scilib.ai/kg/mathlib#List.shortlex_def

English

Shortlex r s t holds iff either |s| < |t| or |s| = |t| and Lex r s t.

Русский

Shortlex r s t выполняется тогда, когда либо |s| < |t|, либо |s| = |t| и Lex r s t.

LaTeX

$$$ \\mathrm{Shortlex} \\ r \\ s \\ t \\iff |s| < |t| \\lor (|s| = |t| \\land \\mathrm{Lex} \\ r \\ s \\ t).$$$

Lean4

theorem shortlex_def {s t : List α} : Shortlex r s t ↔ s.length < t.length ∨ s.length = t.length ∧ Lex r s t :=
  Prod.lex_def

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

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

Разделы

Аффилиация

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