English
If f is a uniform embedding, then the two-sided controls hold: (i) for every ε>0 there exists δ>0 such that dist a b < δ implies dist(f a, f b) < ε; (ii) for every δ>0 there exists ε>0 such that dist(f a, f b) < ε implies dist a b < δ.
Русский
Если f — равномерное вложение, выполняются две стороны контроля: (i) ∀ ε>0 ∃ δ>0: dist(a,b)<δ ⇒ dist(f a,f b)<ε; (ii) ∀ δ>0 ∃ ε>0: dist(f a,f b)<ε ⇒ dist(a,b)<δ.
LaTeX
$$$\\text{IsUniformEmbedding}(f) \\Rightarrow (\\forall ε>0, \\exists δ>0, \\forall a,b, dist(a,b)<δ \\Rightarrow dist(f a,f b)<ε) \\land (\\forall δ>0, \\exists ε>0, \\forall a,b, dist(f a,f b)<ε \\Rightarrow dist(a,b)<δ)$$$
Lean4
/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is an open ball
centered at `x` and intersecting `s` only at `x`. -/
theorem exists_ball_inter_eq_singleton_of_mem_discrete [DiscreteTopology s] {x : α} (hx : x ∈ s) :
∃ ε > 0, Metric.ball x ε ∩ s = { x } :=
nhds_basis_ball.exists_inter_eq_singleton_of_mem_discrete hx
