insert — Mathlib

English

If s is PWOn by r, then inserting an element a into s preserves PWOn by r.

Русский

Если s PWOn по r, то вставка элемента a в s сохраняет PWOn по r.

LaTeX

$$$\\\\text{partiallyWellOrderedOn_insert} : (s.PartiallyWellOrderedOn r) \\\\to \\\\forall a, (insert a s).PartiallyWellOrderedOn r$$$

Lean4

protected theorem insert (h : PartiallyWellOrderedOn s r) (a : α) : PartiallyWellOrderedOn (insert a s) r :=
  partiallyWellOrderedOn_insert.2 h

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