Theorems · Inductive type · general topology

IsUniformInducing

{α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Prop

A map f : α → β between uniform spaces is called uniform inducing if the uniformity filter on α is the pullback of the uniformity filter on β under Prod.map f f. If α is a separated space, then this implies that f is injective, hence it is a IsUniformEmbedding.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

128 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

UniformSpaceUniformSpace