English
If f is IsUniformInducing, then f[s] is totally bounded iff s is totally bounded.
Русский
Если f — исUniformInducing, тогда образ s под f, f[s], полностью ограничен тогда и только тогда, когда s полностью ограничено.
LaTeX
$$$\text{For } f:\alpha \to \beta \text{ with } IsUniformInducing(f),\; (f''s)\text{ is totally bounded }\Leftrightarrow s\text{ is totally bounded}.$$$
Lean4
theorem totallyBounded_image_iff {f : α → β} {s : Set α} (hf : IsUniformInducing f) :
TotallyBounded (f '' s) ↔ TotallyBounded s :=
by
refine ⟨fun hs ↦ ?_, fun h ↦ h.image hf.uniformContinuous⟩
simp_rw [(hf.basis_uniformity (basis_sets _)).totallyBounded_iff]
intro t ht
rcases exists_subset_image_finite_and.1 (hs.exists_subset ht) with ⟨u, -, hfin, h⟩
use u, hfin
rwa [biUnion_image, image_subset_iff, preimage_iUnion₂] at h
