prod_lex — Mathlib

English

If ra and rb are well-founded, then the lexicographic order on the product is well-founded.

Русский

Если ra и rb хорошо основаны, то лексикографический порядок на произведении хорошо основан.

LaTeX

$$$\\forall \\alpha \\; \\forall \\beta \\; \\forall ra rb,\\; \\text{WellFounded } ra \\to \\text{WellFounded } rb \\to \\text{WellFounded } (Prod.Lex ra rb)$$$

Lean4

theorem prod_lex {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra) (hb : WellFounded rb) :
    WellFounded (Prod.Lex ra rb) :=
  (Prod.lex ⟨_, ha⟩ ⟨_, hb⟩).wf

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