instIsWellFoundedTransGen — Mathlib

English

If a relation r on α is well-founded, then the relation TransGen r on α is also well-founded.

Русский

Если отношение r на α хорошо основано, то отношение TransGen r также хорошо основано.

LaTeX

$$$[\text{IsWellFounded } \alpha\ r] \Rightarrow IsWellFounded(\alpha, \text{Relation.TransGen } r)$$$

Lean4

instance (r : α → α → Prop) [i : IsWellFounded α r] : IsWellFounded α (Relation.TransGen r) :=
  ⟨i.wf.transGen⟩

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