iff_forall_not_isBadSeq — Mathlib

English

A set s is partially well-ordered by r iff every possible f: ℕ → α is not a bad sequence contained in s.

Русский

Множество s частично хорошо упорядовано по r тогда и только тогда, когда для всякой функции f: ℕ → α не существует плохой последовательности, лежащей в s.

LaTeX

$$s.PartiallyWellOrderedOn r ↔ ∀ f, ¬IsBadSeq r s f$$

Lean4

theorem iff_forall_not_isBadSeq (r : α → α → Prop) (s : Set α) : s.PartiallyWellOrderedOn r ↔ ∀ f, ¬IsBadSeq r s f :=
  by
  rw [partiallyWellOrderedOn_iff_exists_lt]
  exact forall_congr' fun f => by simp [IsBadSeq]

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