English
If a family of complete sets s_i are pairwise separated by a fixed entourage U, then their union over i is complete.
Русский
Если семейство множества s_i полно и разделено между собой по фиксированной окрестности U, то объединение по i тоже полно.
LaTeX
$$$\\bigl(\\forall i, IsComplete(s_i)\\bigr) \\to \\forall U\\in 𝓤(α),\\ (\\forall i j, x\\in s_i, y\\in s_j, (x,y)\\in U \\Rightarrow i=j) \\to IsComplete(\\bigcup_i s_i)$$$
Lean4
theorem isComplete_iUnion_separated {ι : Sort*} {s : ι → Set α} (hs : ∀ i, IsComplete (s i)) {U : Set (α × α)}
(hU : U ∈ 𝓤 α) (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) : IsComplete (⋃ i, s i) :=
by
set S := ⋃ i, s i
intro l hl hls
rw [le_principal_iff] at hls
obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl
obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U :=
by
rcases hl' U hU with ⟨t, htl, htU⟩
refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
gcongr <;> apply inter_subset_left
obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
refine ⟨i, fun y hy => ?_⟩
rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩
exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩
