insert

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.IsWF.insert

English

If s is well-founded, then inserting an element a into s yields a well-founded set.

Русский

Если s сильно основано, то вставка элемента a в s сохраняет это свойство.

LaTeX

$$$\\operatorname{IsWF}(s) \\Rightarrow \\operatorname{IsWF}(\\operatorname{insert} a\\, s)$$$

Lean4

protected theorem insert (h : IsWF s) (a : α) : IsWF (insert a s) :=
  isWF_insert.2 h

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

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

Разделы

Аффилиация

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