English
Equivalent reformulation: the PWOn property is equivalent to the nonexistence of a globally min-bad sequence.
Русский
Равносильное переформулирование: PWOn эквивалентно несуществованию глобальной минимальной плохой последовательности.
LaTeX
$$∀ {r} {s}, s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f$$
Lean4
/-- Higman's Lemma, which states that for any reflexive, transitive relation `r` which is
partially well-ordered on a set `s`, the relation `List.SublistForall₂ r` is partially
well-ordered on the set of lists of elements of `s`. That relation is defined so that
`List.SublistForall₂ r l₁ l₂` whenever `l₁` related pointwise by `r` to a sublist of `l₂`. -/
theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsPreorder α r] {s : Set α}
(h : s.PartiallyWellOrderedOn r) :
{l : List α | ∀ x, x ∈ l → x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r) :=
by
rcases isEmpty_or_nonempty α
· exact subsingleton_of_subsingleton.partiallyWellOrderedOn
inhabit α
rw [iff_not_exists_isMinBadSeq List.length]
rintro ⟨f, hf1, hf2⟩
have hnil : ∀ n, f n ≠ List.nil := fun n con => hf1.2 n n.succ n.lt_succ_self (con.symm ▸ List.SublistForall₂.nil)
obtain ⟨g, hg⟩ := h.exists_monotone_subseq fun n => hf1.1 n _ (List.head!_mem_self (hnil n))
have hf' :=
hf2 (g 0) (fun n => if n < g 0 then f n else List.tail (f (g (n - g 0)))) (fun m hm => (if_pos hm).symm) ?_
swap
· simp only [if_neg (lt_irrefl (g 0)), Nat.sub_self]
rw [List.length_tail, ← Nat.pred_eq_sub_one]
exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero_iff.1 con)
rw [IsBadSeq] at hf'
push_neg at hf'
obtain ⟨m, n, mn, hmn⟩ :=
hf' fun n x hx => by
split_ifs at hx with hn
exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]
by_cases hn : n < g 0
· apply hf1.2 m n mn
rwa [if_pos hn, if_pos (mn.trans hn)] at hmn
· obtain ⟨n', rfl⟩ := Nat.exists_eq_add_of_le (not_lt.1 hn)
rw [if_neg hn, add_comm (g 0) n', Nat.add_sub_cancel_right] at hmn
split_ifs at hmn with hm
· apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
exact _root_.trans hmn (List.tail_sublistForall₂_self _)
· rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn
apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn
