isWellFounded — Mathlib

English

If r is a well-founded relation on α and s is a subrelation of r, then s is also well-founded on α.

Русский

Если $r$ — хорошо основанное отношение на $\alpha$, а $s$ — подпорядок относительно $r$, то $s$ тоже хорошо основан на $\alpha$.

LaTeX

$$IsWellFounded α s$$

Lean4

theorem isWellFounded (r : α → α → Prop) [IsWellFounded α r] {s : α → α → Prop} (h : Subrelation s r) :
    IsWellFounded α s :=
  ⟨h.wf IsWellFounded.wf⟩

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