English
Let r be a strict order on a set α and s ⊆ α. Then the well-foundedness of r on s is equivalent to the well-foundedness of r on s without the element a, i.e. removing a single element does not affect whether r is well-founded on the set.
Русский
Пусть r — строгий порядок на α и s ⊆ α. Тогда хорошо основанность r на s эквивалентна хорошо основанности r на s \ {a}; удаление одного элемента не влияет на хорошо основанность.
LaTeX
$$$\\\\mathrm{WellFoundedOn}(s \\setminus \\{a\\}, r) \\\\iff \\\\mathrm{WellFoundedOn}(s, r)$$$
Lean4
@[simp]
theorem wellFoundedOn_sdiff_singleton : WellFoundedOn (s \ { a }) r ↔ WellFoundedOn s r := by
simp only [← wellFoundedOn_insert (a := a), insert_diff_singleton, mem_insert_iff, true_or, insert_eq_of_mem]
