lt_def — Mathlib

English

The sum order defines '<' on α ⊕ β by LiftRel(<)(<); i.e., a < b on the sum iff the lifted relation from a and b holds.

Русский

Порядок суммы задаёт '<' на α ⊕ β через LiftRel(<)(<); то есть a < b на сумме эквивалентно соответствующему поднятому отношению.

LaTeX

$$$a < b \iff \mathrm{LiftRel}(<, <)(a,b)$$$

Lean4

theorem lt_def [LT α] [LT β] {a b : α ⊕ β} : a < b ↔ LiftRel (· < ·) (· < ·) a b :=
  Iff.rfl

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