wellQuasiOrderedLE_iff — Mathlib

English

A WellQuasiOrderedLE structure on α is equivalent to having WellFoundedLT and no infinite antichains under ≤.

Русский

Структура WellQuasiOrderedLE на α эквивалентна существованию WellFoundedLT и отсутствию безконечных антицепей по отношению ≤.

LaTeX

$$$\\mathrm{WellQuasiOrderedLE}(\\alpha) \\iff \\mathrm{WellFoundedLT}(\\alpha) \\wedge \\forall s:\\mathrm{Set}(\\alpha),\\ \\mathrm{IsAntichain}(\\le, s) \\Rightarrow s.Finite$$$

Lean4

/-- A preorder is well quasi-ordered iff it's well-founded and has no infinite antichains. -/
theorem wellQuasiOrderedLE_iff :
    WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ s : Set α, IsAntichain (· ≤ ·) s → s.Finite :=
  by
  refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩, fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩
  obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f
  · exfalso
    apply RelEmbedding.not_wellFounded _ hwf.wf
    exact (RelEmbedding.ofMonotone _ h1).swap
  · contrapose! hc
    refine ⟨Set.range (f ∘ g), ?_, ?_⟩
    · rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))
    · refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_
      obtain h | rfl | h := lt_trichotomy m n <;>
        (first
          | rfl
          | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

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