shortlex_singleton_iff

Mathlib.Data.List.Shortlex

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

← MathLib Explorer

English

Shortlex r [a] [b] holds iff r a b.

Русский

Shortlex r [a] [b] выполняется тогда и только тогда, когда r a b.

LaTeX

$$$ \\mathrm{Shortlex} \\ r [a] [b] \\iff r a b.$$$

Lean4

@[simp]
theorem shortlex_singleton_iff (a b : α) : Shortlex r [a] [b] ↔ r a b := by
  simp only [shortlex_def, length_singleton, lt_self_iff_false, lex_singleton_iff, true_and, false_or]

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

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

Разделы

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

Аффилиация

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