le_def — Mathlib

English

The sum order satisfies that a ≤ b on α ⊕ β exactly when LiftRel(≤)(≤) a b holds; i.e., the canonical lifting of the componentwise order defines the sum-order relation.

Русский

Порядок суммы удовлетворяет равенству: a ≤ b на α ⊕ β тогда и только тогда, когда выполняется LiftRel(≤)(≤) a b; то есть каноническое соответствие компонентного порядка задает порядок суммы.

LaTeX

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

Lean4

theorem le_def [LE α] [LE β] {a b : α ⊕ β} : a ≤ b ↔ LiftRel (· ≤ ·) (· ≤ ·) a b :=
  Iff.rfl

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