English
Characterization of uniform inducement: a map is uniform inducing if and only if it is uniformly continuous and its inverse images of Cauchy filters are Cauchy.
Русский
Характеризация условности униформности: отображение является uniform inducing если и только если оно равномерно непрерывно и обратные изображения Cauchy-фильтров являются Cauchy.
LaTeX
$$$f: \alpha \to \beta$ isUniformInducing \iff UniformContinuous f \wedge \forall δ>0, \exists ε>0, ∀{a,b}, edist a b < ε \Rightarrow edist(f a, f b) < δ$.$$
Lean4
theorem isUniformInducing_iff [PseudoEMetricSpace β] {f : α → β} :
IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ :=
isUniformInducing_iff'.trans <|
Iff.rfl.and <|
((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).trans <| by
simp only [subset_def, Prod.forall]; rfl
