partiallyWellOrderedOn — Mathlib

English

Any finite set of elements, viewed as a subset of α, is partially well-ordered under any reflexive relation r.

Русский

Любое конечное множество элементов, рассматриваемое как подмножество α, частично хорошо упорядовано относительно любой рефлексивной связи r.

LaTeX

$$$[IsRefl\\, r] \\; (s: Finset\\alpha).(s:Set).PartiallyWellOrderedOn\\, r$$$

Lean4

@[simp]
protected theorem partiallyWellOrderedOn [IsRefl α r] (s : Finset α) : (s : Set α).PartiallyWellOrderedOn r :=
  s.finite_toSet.partiallyWellOrderedOn

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