English
If there exists a finite discretization witnessing ε-discreteness of s, then s is totally bounded.
Русский
Если существует конечная дискретизация, доказывающая ε-различимость элементов s, то s полностью ограничено.
LaTeX
$$$\\forall ε>0, \\exists β, Fintype(β), F : s\\to β, ∀ x,y\\in s, F x = F y \\Rightarrow d(x,y) < ε \\Rightarrow \\text{TotallyBounded}(s)$$$
Lean4
/-- A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the
space from finitely many data. -/
theorem totallyBounded_of_finite_discretization {s : Set α}
(H : ∀ ε > (0 : ℝ), ∃ (β : Type u) (_ : Fintype β) (F : s → β), ∀ x y, F x = F y → dist (x : α) y < ε) :
TotallyBounded s := by
rcases s.eq_empty_or_nonempty with hs | hs
· rw [hs]
exact totallyBounded_empty
rcases hs with ⟨x0, hx0⟩
haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩
refine totallyBounded_iff.2 fun ε ε0 => ?_
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
let Finv := Function.invFun F
refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
let x' := Finv (F ⟨x, xs⟩)
have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
simp only [Set.mem_iUnion, Set.mem_range]
exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩
