to_wellFoundedLT — Mathlib

English

If α has well-quasi-orderedLE structure, then the order ≤ on α is a WellQuasiOrdered relation.

Русский

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

LaTeX

$$$[LE\\;\\alpha] [WellQuasiOrderedLE\\;\\alpha] : \\mathrm{WellQuasiOrdered}\\ (\\le)$$$

Lean4

instance (priority := 100) to_wellFoundedLT [WellQuasiOrderedLE α] : WellFoundedLT α :=
  by
  rw [WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
  refine ⟨fun f ↦ ?_⟩
  obtain ⟨a, b, h, hf⟩ := wellQuasiOrdered_le f
  exact (f.map_rel_iff.2 h).not_ge hf

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