isPWO_union — Mathlib

English

For any two subsets s and t of α, the union s ∪ t is partially well-ordered if and only if both s and t are partially well-ordered.

Русский

Для любых двух подмножеств s и t множества α объединение s ∪ t частично хорошо упорядочено тогда и только тогда, когда и s, и t частично хорошо упорядочены.

LaTeX

$$$\\operatorname{IsPWO}(s \\cup t) \\iff (\\operatorname{IsPWO}(s) \\land \\operatorname{IsPWO}(t))$$$

Lean4

@[simp]
theorem isPWO_union : IsPWO (s ∪ t) ↔ IsPWO s ∧ IsPWO t :=
  partiallyWellOrderedOn_union

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