isPWO_insert — Mathlib

English

Inserting an element into a PWO set preserves the PWO property.

Русский

Добавление элемента в частично хорошо упорядоченное множество сохраняет свойство PWO.

LaTeX

$$$\\operatorname{IsPWO}(s) \\Rightarrow \\operatorname{IsPWO}(\\operatorname{insert} a\\, s)$$$

Lean4

@[simp]
theorem isPWO_insert {a} : IsPWO (insert a s) ↔ IsPWO s := by
  simp only [← singleton_union, isPWO_union, isPWO_singleton, true_and]

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