isWF_insert — Mathlib

English

The WellFoundedOn relation is preserved by insertion: inserting an element into a set does not change its well-foundedness.

Русский

Вставка элемента в множество сохраняет свойство хорошо основанности относительно данного порядка.

LaTeX

$$$\\operatorname{WellFoundedOn}(\\operatorname{insert} a\\, s, r) \\iff \\operatorname{WellFoundedOn}(s, r)$$$

Lean4

@[simp]
theorem isWF_insert {a} : IsWF (insert a s) ↔ IsWF s := by
  simp only [← singleton_union, isWF_union, isWF_singleton, true_and]

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