instLT

Mathlib.Data.Prod.Lex

URI: https://scilib.ai/kg/mathlib#Prod.Lex.instLT

English

Definition of LT on product via Lex.

Русский

Определение LT на произведении через Lex.

LaTeX

$$LT (Lex (Prod α β))$$

Lean4

instance instLT (α β : Type*) [LT α] [LT β] : LT (α ×ₗ β) where lt := Prod.Lex (· < ·) (· < ·)

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

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

Разделы

Аффилиация

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