English
IsMinBadSeq(r, rk, s, n, f) says that among all bad sequences that agree with f on the first n terms, the rank rk at position n is minimal; more precisely, for any g agreeing with f on the first n terms, if g is a bad sequence, then rk(g(n)) ≥ rk(f(n)).
Русский
IsMinBadSeq(r, rk, s, n, f) означает, что среди всех плохих последовательностей, совпадающих с f на первых n термах, ранг в позиции n минимален; для любого g с тем же свойством ранга.
LaTeX
$$IsMinBadSeq (r) (rk) (s) (n) (f) : ∀ g, (∀ m, m < n → f m = g m) → rk (g n) < rk (f n) → ¬IsBadSeq r s g$$
Lean4
/-- This indicates that every bad sequence `g` that agrees with `f` on the first `n`
terms has `rk (f n) ≤ rk (g n)`. -/
def IsMinBadSeq (r : α → α → Prop) (rk : α → ℕ) (s : Set α) (n : ℕ) (f : ℕ → α) : Prop :=
∀ g : ℕ → α, (∀ m : ℕ, m < n → f m = g m) → rk (g n) < rk (f n) → ¬IsBadSeq r s g
