Theorems · Theorem · general topology
IsUniformInducing.uniformContinuous
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
IsUniformInducing f → UniformContinuous f- Cited by
- 35 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpaceUniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- UniformSpacestatement and proof · cited by 2,040
- UniformContinuousstatement · cited by 410
- IsUniformInducingstatement and proof · cited by 128
- isUniformInducing_iff'proof · cited by 5
Cited by35
Results whose statement or proof uses this declaration.
- AbstractCompletion.uniformContinuous_coeproof · cited by 8
- TopologicalSpace.Closeds.uniformContinuous_coeproof · cited by 5
- TopologicalSpace.NonemptyCompacts.uniformContinuous_coeproof · cited by 4
- TopologicalSpace.Compacts.uniformContinuous_coeproof · cited by 4
- Filter.totallyBounded_map_iffproof · cited by 2
- ContinuousMultilinearMap.uniformContinuous_coe_funproof · cited by 2
- IsDenseInducing.isUniformInducing_extendproof · cited by 1
- ContinuousAlternatingMap.uniformContinuous_toContinuousMultilinearMapproof · cited by 1
- IsUniformInducing.compacts_mapstatement and proof · cited by 1
- IsUniformInducing.isUniformAddGroupproof · cited by 1
- IsUniformInducing.isUniformGroupproof · cited by 1
- TopologicalSpace.NonemptyCompacts.uniformContinuous_singletonproof · cited by 1