wellQuasiOrdered_le — Mathlib

English

If α has a WellQuasiOrderedLE structure, then the relation ≤ on α is a WellQuasiOrdered relation.

Русский

Если у типа α есть структура WellQuasiOrderedLE, то отношение ≤ на α является хорошо-квазиупорядоченным.

LaTeX

$$$\\text{[LE }\\alpha]\\ \\text{[WellQuasiOrderedLE }\\alpha]\\Rightarrow \\mathrm{WellQuasiOrdered}(\\lambda x_1 x_2: \\alpha\\. \\ x_1 \\le x_2)$$$

Lean4

theorem wellQuasiOrdered_le [LE α] [h : WellQuasiOrderedLE α] : @WellQuasiOrdered α (· ≤ ·) :=
  h.wqo

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