iff_not_exists_isMinBadSeq — Mathlib

English

The construction of a minimal bad sequence proceeds by a recursive choice ensuring the agreement on earlier indices and preserving badness and minimality properties at each step.

Русский

Построение минимальной плохой последовательности выполняется рекурсивным выбором, сохраняющим согласованность на ранее выбранных индексах и свойства плохости и минимальности на каждом шаге.

LaTeX

$$IsMinBadSeq construction described above$$

Lean4

theorem iff_not_exists_isMinBadSeq (rk : α → ℕ) {s : Set α} :
    s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f :=
  by
  rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]
  constructor
  · apply exists_min_bad_of_exists_bad
  · rintro ⟨f, hf1, -⟩
    exact ⟨f, hf1⟩

Похожие утверждения