English
If the uniform space has a basis given by a family of entourages with a HasBasis structure, then interUnionBalls(xs,u,V) is TotallyBounded.
Русский
Если у равномерного пространства есть база опоясания через семейство окружностей, заданное HasBasis, то interUnionBalls(xs,u,V) тотально ограничено.
LaTeX
$$$TotallyBounded(\operatorname{interUnionBalls}(xs,u,U))$$$
Lean4
theorem totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)} (H : (uniformity α).HasBasis p U)
(xs : ℕ → α) (u : ℕ → ℕ) : TotallyBounded (interUnionBalls xs u U) :=
by
rw [Filter.HasBasis.totallyBounded_iff H]
intro i _
have h_subset : interUnionBalls xs u U ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) := fun x hx ↦
Set.mem_iInter.1 hx i
classical
refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
iUnion_iUnion_eq_right, Nat.lt_succ_iff]
exact h_subset hx
