English
Every sequence e: ℕ → α with values in S ∪ T has an infinite subsequence taking values entirely in S or entirely in T.
Русский
Любая последовательность e: ℕ → α, значения которой лежат в S ∪ T, имеет бесконечную подпоследовательность, значения которой лежат целиком либо в S, либо в T.
LaTeX
$$$$\exists g:\mathbb{N} \hookrightarrow_o \mathbb{N},\ (\forall n, e(g(n)) \in s) \lor (\forall n, e(g(n)) \in t).$$$$
Lean4
theorem exists_subseq_of_forall_mem_union {s t : Set α} (e : ℕ → α) (he : ∀ n, e n ∈ s ∪ t) :
∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ ∀ n, e (g n) ∈ t := by
classical
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
cases this
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
