isPWO — Mathlib

English

If α is a preorder, then a finite set s viewed as a set is partially well-ordered on α.

Русский

Если α образует предраorder, то конечное множество s, рассматриваемое как множество над α, частично хорошо упорядовано.

LaTeX

$$$[Preorder\\, α] (s: Finset\\, α) \\Rightarrow (↑s : Set\\, α).IsPWO$$$

Lean4

@[simp]
protected theorem isPWO [Preorder α] (s : Finset α) : Set.IsPWO (↑s : Set α) :=
  s.partiallyWellOrderedOn

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