Mathlib Map

Theorems · Theorem · general topology

UniformSpace.Completion.denseRange_coe

∀ {α : Type u_1} [inst : UniformSpace α], DenseRange UniformSpace.Completion.coe'
Defined in
Mathlib.Topology.UniformSpace.Completion
Cited by
9 results in Mathlib
Foundations
Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
UniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

UniformSpace.Completion.cPkg · cited by 23Completion.cPkgUniformSpace.Completion.isDenseInducing_coe · cited by 11Completion.isDenseInducin…UniformSpace.Completion.induction_on · cited by 8Completion.induction_onValued.continuous_extension · cited by 2Valued.continuous_extensi…UniformSpace.Completion.denseRange_coe₂ · cited by 2Completion.denseRange_coe₂NumberField.InfinitePlace.Completion.denseRange_coe · cited by 1Completion.denseRange_coeValued.closure_coe_completion_v_lt · cited by 1Valued.closure_coe_comple…UniformSpace.Completion.denseRange_coe₃ · cited by 1Completion.denseRange_coe₃IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap · cited by 0HeightOneSpectrum.denseRa…Valued.exists_coe_eq_v · cited by 0Valued.exists_coe_eq_vUniformSpace · cited by 2040UniformSpaceUniformSpace.Completion · cited by 192UniformSpace.CompletionDenseRange · cited by 164DenseRangeUniformSpace.Completion.coe' · cited by 144Completion.coe'Function.Surjective.denseRange · cited by 21Surjective.denseRangeSeparationQuotient.surjective_mk · cited by 12SeparationQuotient.surjec…SeparationQuotient.continuous_mk · cited by 9SeparationQuotient.contin…DenseRange.comp · cited by 9DenseRange.compCauchyFilter.denseRange_pureCauchy · cited by 5CauchyFilter.denseRange_p…Completion.denseRange_coeCITED BYCITES

Cites9

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

Cited by10

Results whose statement or proof uses this declaration.