English
For a map f between pseudometric spaces, IsUniformInducing f is equivalent to UniformContinuous f together with a δ–ε control: for every δ>0 there exists ε>0 such that if dist(f a, f b) < ε then dist(a, b) < δ.
Русский
Для отображения f между псевдометрическими пространствами, IsUniformInducing f эквивалентно тому, что f равномерно непрерывно и существует управление δ–ε: для каждого δ>0 существует ε>0 такое, что dist(f a, f b) < ε ⇒ dist(a, b) < δ.
LaTeX
$$$\\text{IsUniformInducing}(f) \\iff \\text{UniformContinuous}(f) \\land \\forall \\delta>0, \\exists \\varepsilon>0, \\forall a,b, dist(f(a),f(b))<\\varepsilon \\Rightarrow dist(a,b)<\\delta$$$
Lean4
nonrec theorem isUniformInducing_iff [PseudoMetricSpace β] {f : α → β} :
IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
isUniformInducing_iff'.trans <|
Iff.rfl.and <|
((uniformity_basis_dist.comap _).le_basis_iff uniformity_basis_dist).trans <| by
simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf]
