English
Given a bad sequence f, this constructs a new bad sequence g that agrees with f on the first n terms and is minimal at n, in a way that preserves badness and a minimality property.
Русский
Дано плохую последовательность f; строится новая плохая последовательность g, совпадающая с f на первых n термах и минимальная в позиции 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
/-- In the context of partial well-orderings, a bad sequence is a nonincreasing sequence
whose range is contained in a particular set `s`. One exists if and only if `s` is not
partially well-ordered. -/
def IsBadSeq (r : α → α → Prop) (s : Set α) (f : ℕ → α) : Prop :=
(∀ n, f n ∈ s) ∧ ∀ m n : ℕ, m < n → ¬r (f m) (f n)
