sdiff_singleton — Mathlib

English

If s is well-founded with respect to r, then removing a single element a from s preserves well-foundedness with respect to r.

Русский

Если s хорошо основано относительно r, то s \\ {a} сохраняет хорошо основанность относительно r.

LaTeX

$$$\\\\mathrm{WellFoundedOn}(s \\setminus \\{a\\}, r)$$$

Lean4

protected theorem sdiff_singleton (h : WellFoundedOn s r) (a : α) : WellFoundedOn (s \ { a }) r :=
  wellFoundedOn_sdiff_singleton.2 h

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