insert — Mathlib

English

If a set s is well-founded with respect to a relation r, then adding any element a to s preserves well-foundedness with respect to r.

Русский

Если множество s хорошо основано относительно отношения r, то добавление любого элемента a сохраняет хорошо основанность относительно r.

LaTeX

$$$\\\\mathrm{WellFoundedOn}(\\\\text{insert}(a, s), r) \\\\text{ whenever } s\\\\text{ is WellFoundedOn } r$$$

Lean4

protected theorem insert (h : WellFoundedOn s r) (a : α) : WellFoundedOn (insert a s) r :=
  wellFoundedOn_insert.2 h

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