IsPWO — Mathlib

English

If s is an antichain with respect to r, then s is PWOn by r if and only if s is finite.

Русский

Если s является антицепью по отношению к r, то s PWOn по r тогда и только тогда, когда s конечна.

LaTeX

$$IsAntichain r s → (s.PartiallyWellOrderedOn r ↔ s.Finite)$$

Lean4

/-- A subset of a preorder is partially well-ordered when any infinite sequence contains
  a monotone subsequence of length 2 (or equivalently, an infinite monotone subsequence). -/
def IsPWO (s : Set α) : Prop :=
  PartiallyWellOrderedOn s (· ≤ ·)

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