wellFounded — Mathlib

English

Well-foundedness is preserved under a RelEmbedding: if f : r ↪r s and s is well-founded, then r is well-founded.

Русский

Хорошо основанность сохраняется через вложение: если f : r ↪r s и s хорошо основано, то r тоже хорошо основано.

LaTeX

$$$\forall f:(r\hookrightarrow s),\\text{WellFounded}(s) \Rightarrow \text{WellFounded}(r)$$$

Lean4

protected theorem wellFounded : ∀ (_ : r ↪r s) (_ : WellFounded s), WellFounded r
  | f, ⟨H⟩ => ⟨fun _ => f.acc _ (H _)⟩

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