wellFounded — Mathlib

English

If there is a relation-homomorphism from r to s and s is well-founded, then r is well-founded.

Русский

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

LaTeX

$$$\operatorname{WellFounded} s \Rightarrow \operatorname{WellFounded} r$$$

Lean4

protected theorem wellFounded [RelHomClass F r s] (f : F) : WellFounded s → WellFounded r
  | ⟨H⟩ => ⟨fun _ => RelHomClass.acc f _ (H _)⟩

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