le_iff' — Mathlib

English

A partial-order variant: x ≤ y is equivalent to the first components comparison plus a conditional second component bound.

Русский

Вариант для частичного порядка: x ≤ y эквивалентно сравнению первых координат с условием на вторую координату.

LaTeX

$$$$ x \le y \iff x_1 \le y_1 \land (x_1 = y_1 \rightarrow x_2 \le y_2). $$$$

Lean4

/-- Variant of `Prod.Lex.le_iff` for partial orders. -/
theorem le_iff' {x y : α ×ₗ β} :
    x ≤ y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 ≤ (ofLex y).2) :=
  toLex_le_toLex'

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