English
Let s be a transitive relation on β. Then s is well-founded iff every induced subrelation r ≺i s is well-founded.
Русский
Пусть s — транзитивное отношение на β. Тогда s является хорошо упорядоченным (well-founded), если и только если каждая породненная подотношение r ≺i s также хорошо упорядочено.
LaTeX
$$$\text{WellFounded } s \iff \forall \alpha\, (r:\alpha \to \alpha \to \mathrm{Prop})\, (\, r \prec i\ s\,) \Rightarrow \text{WellFounded } r$$$
Lean4
theorem wellFounded_iff_principalSeg {β : Type u} {s : β → β → Prop} [IsTrans β s] :
WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop) (_ : r ≺i s), WellFounded r :=
⟨fun wf _ _ f => RelHomClass.wellFounded f.toRelEmbedding wf, fun h =>
wellFounded_iff_wellFounded_subrel.mpr fun b => h _ _ (PrincipalSeg.ofElement s b)⟩
