Theorems · Definition · general topology
TopologicalSpace.NonemptyCompacts.toCompacts
{α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.NonemptyCompacts α → TopologicalSpace.Compacts α- Defined in
- Mathlib.Topology.Sets.Compacts
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- TopologicalSpace.Compactsstatement · cited by 386
- TopologicalSpace.NonemptyCompactsstatement and proof · cited by 137
Cited by28
Results whose statement or proof uses this declaration.
- TopologicalSpace.NonemptyCompacts.mapproof · cited by 18
- TopologicalSpace.NonemptyCompacts.isEmbedding_toCompactsstatement · cited by 12
- TopologicalSpace.NonemptyCompacts.continuous_toCompactsstatement · cited by 8
- TopologicalSpace.NonemptyCompacts.range_toCompactsstatement and proof · cited by 5
- TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompactsstatement and proof · cited by 5
- TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompactsstatement and proof · cited by 5
- TopologicalSpace.NonemptyCompacts.toCompactsOrderEmbeddingproof · cited by 3
- TopologicalSpace.NonemptyCompacts.isCompactproof · cited by 2
- TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompactproof · cited by 2
- TopologicalSpace.NonemptyCompacts.toCompacts_injectivestatement · cited by 2
- TopologicalSpace.NonemptyCompacts.coe_toCompactsOrderEmbeddingstatement · cited by 2
- TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompactsstatement · cited by 2