instIsWellFoundedInvImage — Mathlib

English

If r is a well-founded relation on α and f : β → α, then the inverse-image relation on β, InvImage r f, is well-founded.

Русский

Если отношение $r$ на $\alpha$ хорошо основано, и есть функция $f:\beta\to\alpha$, то отношение на $\beta$, заданное по обратному образу $InvImage\,r\,f$, хорошо основано.

LaTeX

$$IsWellFounded(β, InvImage(r,f))$$

Lean4

instance (r : α → α → Prop) [IsWellFounded α r] (f : β → α) : IsWellFounded _ (InvImage r f) :=
  ⟨InvImage.wf f IsWellFounded.wf⟩

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