English
Given a bad sequence, construct a bad sequence g that agrees with f up to n and carries a minimal bad-sequence property via rk.
Русский
Существование минимальной плохой последовательности: дана плохая последовательность f, строится g, которая совпадает с f до n-го элемента и обладает минимальностью.
LaTeX
$$minBadSeqOfBadSeq (r) (rk) (s) (n) (f) (hf) : { g : ℕ → α // (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }$$
Lean4
/-- Given a bad sequence `f`, this constructs a bad sequence that agrees with `f` on the first `n`
terms and is minimal at `n`.
-/
noncomputable def minBadSeqOfBadSeq (r : α → α → Prop) (rk : α → ℕ) (s : Set α) (n : ℕ) (f : ℕ → α)
(hf : IsBadSeq r s f) : { g : ℕ → α // (∀ m : ℕ, m < n → f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g } :=
by
classical
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
⟨_, f, fun _ _ => rfl, hf, rfl⟩
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
refine ⟨Classical.choose (Nat.find_spec h), h1, by convert h2, fun g hg1 hg2 con => ?_⟩
refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
rwa [← h3]
