partiallyWellOrderedOn_iff — 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 частично хорошо упорядочено по r тогда и только тогда, когда s конечна.

LaTeX

$$$IsAntichain r s \\Rightarrow (s.PartiallyWellOrderedOn r \\iff s.Finite)$$$

Lean4

theorem _root_.IsAntichain.partiallyWellOrderedOn_iff (hs : IsAntichain r s) : s.PartiallyWellOrderedOn r ↔ s.Finite :=
  ⟨hs.finite_of_partiallyWellOrderedOn, Finite.partiallyWellOrderedOn⟩

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