wellFoundedOn_union — Mathlib

English

The WellFoundedOn property for a union is equivalent to the conjunction of the respective WellFoundedOn properties for the parts.

Русский

Свойство WellFoundedOn для объединения эквивалентно конъюнкции соответствующих WellFoundedOn для частей.

LaTeX

$$∀ {α} {r} {s t : Set α}, (s.WellFoundedOn r ∧ t.WellFoundedOn r) ⇔ (s ∪ t).WellFoundedOn r$$

Lean4

@[simp]
theorem wellFoundedOn_union : (s ∪ t).WellFoundedOn r ↔ s.WellFoundedOn r ∧ t.WellFoundedOn r :=
  ⟨fun h => ⟨h.subset subset_union_left, h.subset subset_union_right⟩, fun h => h.1.union h.2⟩

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