Mathlib Map

Theorems · Theorem · general topology

IsUniformEmbedding.isUniformInducing

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformEmbedding f → IsUniformInducing f
Defined in
Mathlib.Topology.UniformSpace.Defs
Cited by
33 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
UniformSpaceUniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsUniformEmbedding.of_comp_iff · cited by 8IsUniformEmbedding.of_com…LinearMap.extendOfNorm_eq · cited by 7LinearMap.extendOfNorm_eqIsUniformEmbedding.comp · cited by 7IsUniformEmbedding.compIsUniformEmbedding.isClosedEmbedding · cited by 7IsUniformEmbedding.isClos…completeSpace_coe_iff_isComplete · cited by 6completeSpace_coe_iff_isC…MeasureTheory.Lp.simpleFunc.isUniformInducing · cited by 3simpleFunc.isUniformInduc…isUniformEmbedding_iff_isUniformInducing · cited by 2isUniformEmbedding_iff_is…UniformOnFun.postcomp_isUniformEmbedding · cited by 1UniformOnFun.postcomp_isU…IsDenseInducing.isUniformInducing_extend · cited by 1IsDenseInducing.isUniform…IsUniformInducing.compacts_map · cited by 1IsUniformInducing.compact…IsUniformInducing.nonemptyCompacts_map · cited by 1IsUniformInducing.nonempt…LinearPMap.adjointDomainMkCLMExtend_apply · cited by 1LinearPMap.adjointDomainM…ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM · cited by 1ContinuousAlternatingMap.…UniformConvergenceCLM.isUniformEmbedding_postcomp · cited by 1UniformConvergenceCLM.isU…ContinuousLinearMap.opNorm_extend_le · cited by 1ContinuousLinearMap.opNor…UniformSpace · cited by 2040UniformSpaceIsUniformInducing · cited by 128IsUniformInducingIsUniformEmbedding · cited by 107IsUniformEmbeddingIsUniformEmbedding.toIsUniformInducing · cited by 44IsUniformEmbedding.toIsUn…IsUniformEmbedding.isUniformI…CITED BYCITES

Cites4

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

Cited by33

Results whose statement or proof uses this declaration.