isWellFounded

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelEmbedding.isWellFounded

English

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{IsWellFounded } s] \Rightarrow \text{IsWellFounded } r$$$

Lean4

protected theorem isWellFounded (f : r ↪r s) [IsWellFounded β s] : IsWellFounded α r :=
  ⟨f.wellFounded IsWellFounded.wf⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru