partiallyWellOrderedOn_union — Mathlib

English

The partially well-ordered property for a union is equivalent to the pair of subfamilies being PWOn.

Русский

Свойство частично хорошо упорядоченного для объединения эквивалентно тому, что каждая часть является PWOn.

LaTeX

$$$(s.PartiallyWellOrderedOn r) \\leftrightarrow (t.PartiallyWellOrderedOn r) \\Rightarrow ((s \\cup t).PartiallyWellOrderedOn r)$$$

Lean4

@[simp]
theorem partiallyWellOrderedOn_union :
    (s ∪ t).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r ∧ t.PartiallyWellOrderedOn r :=
  ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun h ↦ h.1.union h.2⟩

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