inl_lt_inr

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.Lex.inl_lt_inr

English

For all a in α and b in β, we have toLex(inl a) < toLex(inr b).

Русский

Для всех a ∈ α и b ∈ β имеем toLex(inl a) < toLex(inr b).

LaTeX

$$$\forall a:\, a \in \alpha,\; \forall b:\, b \in \beta:\; toLex(\mathrm{Sum.inl}(a)) < toLex(\mathrm{Sum.inr}(b)).$$$

Lean4

theorem inl_lt_inr [LT α] [LT β] (a : α) (b : β) : toLex (inl a) < toLex (inr b) :=
  Lex.sep _ _

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

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

Разделы

Аффилиация

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