English
A set s is PWOn r iff there does not exist a bad sequence f in s that is bad at every index with the minimal bad-sequence property.
Русский
Множество s частично хорошо упорядовано по r тогда, когда не существует плохой последовательности f в s, удовлетворяющей всем условиям минимальности.
LaTeX
$$s.PartiallyWellOrderedOn r \leftrightarrow \neg\exists f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f$$
Lean4
theorem exists_min_bad_of_exists_bad (r : α → α → Prop) (rk : α → ℕ) (s : Set α) :
(∃ f, IsBadSeq r s f) → ∃ f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f :=
by
rintro ⟨f0, hf0 : IsBadSeq r s f0⟩
let fs : ∀ n : ℕ, { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
by
refine Nat.rec ?_ fun n fn => ?_
· exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩
· exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1, (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩
have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m := fun m n mn =>
by
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn; clear mn
induction k with
| zero => rfl
| succ k
ih =>
rw [ih,
(minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
(Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]
rfl
refine ⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩
· dsimp
rw [h m n mn.le]
exact (fs n).2.1.2 m n mn
· refine (fs n).2.2 g (fun m mn => ?_) hg2
rw [← h m n mn.le, ← hg1 m mn]
