lex_lt_of_lt — Mathlib

English

If r is well-founded and x < y in the Pi-preorder, there exists an index i witnessing a coordinate-wise comparison in the Lex order.

Русский

Если r хорошо упорядочено и x < y в Pi-предпорядке, существует индекс i, свидетельствующий о по координатном сравнении в порядке Lex.

LaTeX

$$$\\exists i\\, (\\forall j, r(j,i) \\to x_j \\le y_j \\wedge y_j \\le x_j) \\land x_i < y_i$$$

Lean4

theorem lex_lt_of_lt [∀ i, PartialOrder (β i)] {r} (hwf : WellFounded r) {x y : ∀ i, β i} (hlt : x < y) :
    Pi.Lex r (· < ·) x y := by
  simp_rw [Pi.Lex, le_antisymm_iff]
  exact lex_lt_of_lt_of_preorder hwf hlt

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