Theorems · Definition · general topology
TopologicalSpace.Compacts.map
{α : Type u_1} →
{β : Type u_2} →
[inst : TopologicalSpace α] →
[inst_1 : TopologicalSpace β] →
(f : α → β) → Continuous f → TopologicalSpace.Compacts α → TopologicalSpace.Compacts βThe image of a compact set under a continuous function.
- Defined in
- Mathlib.Topology.Sets.Compacts
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
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
- Set.imageproof · cited by 5,609
- Continuousstatement and proof · cited by 2,592
- TopologicalSpace.Compactsstatement and proof · cited by 386
- TopologicalSpace.Compacts.carrierproof · cited by 45
Cited by41
Results whose statement or proof uses this declaration.
- TopologicalSpace.NonemptyCompacts.mapproof · cited by 18
- TopologicalSpace.Compacts.equivproof · cited by 7
- TopologicalSpace.PositiveCompacts.mapproof · cited by 7
- TopologicalSpace.CompactOpens.mapproof · cited by 4
- MeasureTheory.Content.innerContent_comapstatement and proof · cited by 3
- Topology.IsEmbedding.compacts_mapstatement · cited by 2
- TopologicalSpace.Compacts.map_injectivestatement · cited by 2
- Continuous.compacts_mapstatement · cited by 2
- TopologicalSpace.Compacts.range_mapstatement · cited by 2
- MeasureTheory.Content.outerMeasure_preimagestatement and proof · cited by 2
- MeasureTheory.Measure.haar.is_left_invariant_addCHaarstatement and proof · cited by 1
- MeasureTheory.Measure.haar.is_left_invariant_addPrehaarstatement · cited by 1