isWellFounded — Mathlib

English

If there exists a RelHom from r to s and s is well-founded, then r is well-founded.

Русский

Если существует отображение, сохраняющее отношение, и отношение s хорошо основано, то и r хорошо основано.

LaTeX

$$$\forall f,\ [\text{RelHomClass } F\ r\ s] \ (\operatorname{IsWellFounded} s) \Rightarrow \operatorname{IsWellFounded} r$$$

Lean4

protected theorem isWellFounded [RelHomClass F r s] (f : F) [IsWellFounded β s] : IsWellFounded α r :=
  ⟨RelHomClass.wellFounded f IsWellFounded.wf⟩

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