wellQuasiOrdered — Mathlib

English

If α is finite and r is reflexive on α, then r is a well-quasi-order.

Русский

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

LaTeX

$$$\\operatorname{Finite}(\\alpha) \\wedge \\operatorname{IsRefl}(\\alpha, r) \\Rightarrow \\mathrm{WellQuasiOrdered}(r)$$$

Lean4

theorem wellQuasiOrdered (r : α → α → Prop) [Finite α] [IsRefl α r] : WellQuasiOrdered r :=
  by
  intro f
  obtain ⟨m, n, h, hf⟩ := Set.finite_univ.exists_lt_map_eq_of_forall_mem (f := f) fun _ ↦ Set.mem_univ _
  exact ⟨m, n, h, hf ▸ refl _⟩

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