Mathlib Map

Theorems · Theorem · general topology

IsUniformInducing.comap_uniformSpace

∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → UniformSpace.comap f inst_1 = inst

Alias of the forward direction of isUniformInducing_iff_uniformSpace.

Defined in
Mathlib.Topology.UniformSpace.UniformEmbedding
Cited by
4 results in Mathlib
Foundations
Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
UniformSpaceUniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsUniformInducing.isInducing · cited by 23IsUniformInducing.isInduc…IsUniformInducing.isUltraUniformity · cited by 2IsUniformInducing.isUltra…UniformFun.comap_eq · cited by 2UniformFun.comap_eqUniformEquiv.comap_eq · cited by 0UniformEquiv.comap_eqUniformSpace · cited by 2040UniformSpaceIsUniformInducing · cited by 128IsUniformInducingUniformSpace.comap · cited by 61UniformSpace.comapisUniformInducing_iff_uniformSpace · cited by 3isUniformInducing_iff_uni…IsUniformInducing.comap_unifo…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.