wellFoundedOn

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#WellFounded.wellFoundedOn

English

If r is well-founded, then its restriction to any subset s is well-founded.

Русский

Если отношение r хорошо основано, то его ограничение на любое подмножество s также хорошо основано.

LaTeX

$$WellFounded r \\Rightarrow s.WellFoundedOn r$$

Lean4

theorem _root_.WellFounded.wellFoundedOn : WellFounded r → s.WellFoundedOn r :=
  InvImage.wf _

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

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

Разделы

Аффилиация

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