English
The image of a totally bounded set under a uniformly continuous map is totally bounded.
Русский
Образ полностью ограниченного множества при равномерно непрерывной карте остаётся полностью ограниченным.
LaTeX
$$$$\\text{TotallyBounded}(s) \\Rightarrow \\text{TotallyBounded}(f[s]) \\text{ for uniformly continuous } f.$$$$
Lean4
/-- The image of a totally bounded set under a uniformly continuous map is totally bounded. -/
theorem image [UniformSpace β] {f : α → β} {s : Set α} (hs : TotallyBounded s) (hf : UniformContinuous f) :
TotallyBounded (f '' s) := fun t ht =>
have : {p : α × α | (f p.1, f p.2) ∈ t} ∈ 𝓤 α := hf ht
let ⟨c, hfc, hct⟩ := hs _ this
⟨f '' c, hfc.image f,
by
simp only [mem_image, iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, image_subset_iff, preimage_iUnion,
preimage_setOf_eq]
have hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t := by simpa [subset_def] using hct
intro x hx
simpa using hct x hx⟩
