lex_iff

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.lex_iff

← MathLib Explorer

English

Prod.Lex r s x y holds iff r x1 y1 or (x1 = y1 and s x2 y2).

Русский

Prod.Lex r s x y выполняется тогда и только тогда, когда r x1 y1 или (x1 = y1 и s x2 y2).

LaTeX

$$$\\\\forall {α} {β} {r} {s} {x y},\\\\n \\\\text{Prod.Lex } r s x y \\\\iff r x.fst y.fst \\\\lor \\\\bigl(x.fst = y.fst \\\\land s x.snd y.snd\\\\bigr).$$$

Lean4

theorem lex_iff : Prod.Lex r s x y ↔ r x.1 y.1 ∨ x.1 = y.1 ∧ s x.2 y.2 :=
  lex_def

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

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

Разделы

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

Аффилиация

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