Theorems · Definition · general topology
TopologicalSpace.Compacts.toCloseds
{α : Type u_1} → [inst : TopologicalSpace α] → [T2Space α] → TopologicalSpace.Compacts α → TopologicalSpace.Closeds αReinterpret a compact as a closed set.
- Defined in
- Mathlib.Topology.Sets.Compacts
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceT2Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- SetLike.coeproof · cited by 8,199
- T2Spacestatement and proof · cited by 1,351
- TopologicalSpace.Compactsstatement and proof · cited by 386
- TopologicalSpace.Closedsstatement · cited by 168
Cited by12
Results whose statement or proof uses this declaration.
- TopologicalSpace.Compacts.isUniformEmbedding_toClosedsstatement · cited by 2
- TopologicalSpace.Compacts.isClosedEmbedding_toClosedsstatement and proof · cited by 1
- TopologicalSpace.Compacts.toCloseds_injectivestatement · cited by 1
- TopologicalSpace.Compacts.isEmbedding_toClosedsstatement · cited by 1
- TopologicalSpace.Compacts.uniformContinuous_toClosedsstatement · cited by 1
- TopologicalSpace.Compacts.isometry_toClosedsstatement · cited by 0
- TopologicalSpace.Compacts.coe_toClosedsstatement and proof · cited by 0
- TopologicalSpace.NonemptyCompacts.toCloseds_toCompactsstatement · cited by 0
- TopologicalSpace.Compacts.toCloseds_prodstatement and proof · cited by 0
- TopologicalSpace.Compacts.toCloseds_singletonstatement · cited by 0
- TopologicalSpace.Compacts.continuous_toClosedsstatement · cited by 0
- TopologicalSpace.Compacts.mem_toClosedsstatement · cited by 0