wellFounded — Mathlib

English

An order embedding preserves well-foundedness: if β is well-founded under <, then α is well-founded under <.

Русский

Вложение порядка сохраняет корректность основания: если β хорошо основано по <, то и α хорошо основано по <.

LaTeX

$$$\\text{WellFounded}((<)_{\\beta}) \\Rightarrow \\text{WellFounded}((<)_{\\alpha})$.$$

Lean4

protected theorem wellFounded (f : α ↪o β) :
    WellFounded ((· < ·) : β → β → Prop) → WellFounded ((· < ·) : α → α → Prop) :=
  f.ltEmbedding.wellFounded

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