toLex_strictMono — Mathlib

English

Verification that toLex preserves strict order: the same as above, stated as a property.

Русский

Подтверждение того, что toLex сохраняет строгий порядок: то же, что и выше, в форме свойства.

LaTeX

$$$$ \text{StrictMono}(\mathrm{toLex}). $$$$

Lean4

theorem toLex_strictMono : StrictMono (toLex : α × β → α ×ₗ β) :=
  by
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
  obtain rfl | ha : a₁ = a₂ ∨ _ := h.le.1.eq_or_lt
  · exact right _ (Prod.mk_lt_mk_iff_right.1 h)
  · exact left _ _ ha

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