wellFoundedOn_insert — Mathlib

English

Inserting an element preserves the well-foundedness of the set under a given order.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem wellFoundedOn_insert : WellFoundedOn (insert a s) r ↔ WellFoundedOn s r := by
  simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and]

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