Theorems · Theorem · general topology
UniformSpace.Completion.uniformContinuous_coe
∀ (α : Type u_1) [inst : UniformSpace α], UniformContinuous UniformSpace.Completion.coe'
- Defined in
- Mathlib.Topology.UniformSpace.Completion
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- UniformSpace.Completionstatement · cited by 192
- UniformSpace.Completion.coe'statement · cited by 144
- UniformSpace.Completion.cPkgproof · cited by 23
- AbstractCompletion.uniformContinuous_coeproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- UniformSpace.Completion.map_compproof · cited by 2
- UniformSpace.Completion.continuous_hatInvproof · cited by 1
- summable_iff_cauchySeq_finset_and_tsum_memproof · cited by 0
- UniformSpace.Completion.mem_uniformity_distproof · cited by 0