isWF — Mathlib

English

Let α be a type with a preorder ≤, and s ⊆ α. If s is partially well-ordered under ≤, then s is well-founded under ≤ restricted to s; equivalently, every nonempty subset of s has a minimal element.

Русский

Пусть α — множество с предикарным порядком ≤, и s ⊆ α. Если s частично хорошо упорядочено по ≤, то ограниченный порядок на s является хорошо основанным; то есть любое непустое подмножество s имеет минимальный элемент.

LaTeX

$$$\\operatorname{IsPWO}(s) \\Rightarrow \\operatorname{IsWF}(s)$$$

Lean4

protected theorem isWF (h : s.IsPWO) : s.IsWF := by simpa only [← lt_iff_le_not_ge] using h.wellFoundedOn

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