union — Mathlib

English

If s and t are WellFoundedOn r, then s ∪ t is WellFoundedOn r.

Русский

Если множества s и t хорошо основаны по r, то их объединение s ∪ t тоже хорошо основано по r.

LaTeX

$$hs : s.WellFoundedOn r → ht : t.WellFoundedOn r → (s ∪ t).WellFoundedOn r$$

Lean4

theorem union (hs : s.WellFoundedOn r) (ht : t.WellFoundedOn r) : (s ∪ t).WellFoundedOn r :=
  by
  rw [wellFoundedOn_iff_no_descending_seq] at *
  rintro f hf
  rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩
  exacts [hs (g.dual.ltEmbedding.trans f) hg, ht (g.dual.ltEmbedding.trans f) hg]

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