union — Mathlib

English

If s and t are partially well-ordered, then their union s ∪ t is partially well-ordered.

Русский

Если s и t частично хорошо упорядочены, то их объединение s ∪ t также частично хорошо упорядочено.

LaTeX

$$$\\operatorname{IsPWO}(s) \\Rightarrow \\operatorname{IsPWO}(t) \\Rightarrow \\operatorname{IsPWO}(s \\cup t)$$$

Lean4

protected nonrec theorem union (hs : IsPWO s) (ht : IsPWO t) : IsPWO (s ∪ t) :=
  hs.union ht

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