English
Finite subfamily again: union over a finite index set is controlled by its parts.
Русский
Ещё раз про биобъединение конечной подпоследовательности: объединение по конечному индексу контролируется по частям.
LaTeX
$$$$TotallyBounded(\\bigcup_{i\\in I} s_i) \\iff \\forall i\\in I, TotallyBounded(s_i).$$$$
Lean4
theorem cauchy_of_totallyBounded {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ 𝓟 s) :
Cauchy (f : Filter α) :=
⟨f.neBot', fun _ ht =>
let ⟨t', ht'₁, ht'_symm, ht'_t⟩ := comp_symm_of_uniformity ht
let ⟨i, hi, hs_union⟩ := hs t' ht'₁
have : (⋃ y ∈ i, {x | (x, y) ∈ t'}) ∈ f := mem_of_superset (le_principal_iff.mp h) hs_union
have : ∃ y ∈ i, {x | (x, y) ∈ t'} ∈ f := (Ultrafilter.finite_biUnion_mem_iff hi).1 this
let ⟨y, _, hif⟩ := this
have : {x | (x, y) ∈ t'} ×ˢ {x | (x, y) ∈ t'} ⊆ compRel t' t' :=
fun ⟨_, _⟩ ⟨(h₁ : (_, y) ∈ t'), (h₂ : (_, y) ∈ t')⟩ => ⟨y, h₁, ht'_symm h₂⟩
mem_of_superset (prod_mem_prod hif hif) (Subset.trans this ht'_t)⟩
