Mathlib Map

Theorems · Theorem · general topology

IsComplete.completeSpace_coe

∀ {α : Type u} [inst : UniformSpace α] {s : Set α}, IsComplete s → CompleteSpace ↑s

Alias of the reverse direction of completeSpace_coe_iff_isComplete.

Defined in
Mathlib.Topology.UniformSpace.UniformEmbedding
Cited by
3 results in Mathlib
Foundations
Depth 77 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.

ContractingWith.exists_fixedPoint' · cited by 4ContractingWith.exists_fi…OrthogonalFamily.isInternal_iff_of_isComplete · cited by 1OrthogonalFamily.isIntern…IsDenseInducing.isUniformInducing_extend · cited by 1IsDenseInducing.isUniform…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemCompleteSpace · cited by 2532CompleteSpaceUniformSpace · cited by 2040UniformSpaceIsComplete · cited by 68IsCompletecompleteSpace_coe_iff_isComplete · cited by 6completeSpace_coe_iff_isC…IsComplete.completeSpace_coeCITED BYCITES

Cites6

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

Cited by3

Results whose statement or proof uses this declaration.