lex_singleton_iff

Mathlib.Data.List.Lex

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

English

For any relation r, and any a,b, Lex r [a] [b] holds if and only if r a b.

Русский

Для любой связи r и элементов a,b выполняется, что Lex r [a] [b] эквивалентно r a b.

LaTeX

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

Lean4

@[simp]
theorem lex_singleton_iff {r : α → α → Prop} (a b : α) : List.Lex r [a] [b] ↔ r a b :=
  ⟨fun
    | .rel h => h, .rel⟩

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

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

Разделы

Аффилиация

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