onFun — Mathlib

English

Let r be a well-founded relation on β and let f: α → β. Then the induced relation on α defined by x ≤ y if r (f x) (f y) is well-founded.

Русский

Пусть r — хорошо основанное отношение на β, и задано отображение f: α → β. Тогда на α, через отношение x ≤ y, если r (f x) (f y), тоже существует хорошо основанное отношение.

LaTeX

$$$\\text{WellFounded } r \\;\\Rightarrow\\; \\text{WellFounded }\\big(\\lambda x y. r (f x) (f y)\\big)$$$

Lean4

theorem onFun {α β : Sort*} {r : β → β → Prop} {f : α → β} : WellFounded r → WellFounded (r on f) :=
  InvImage.wf _

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