Theorems · Theorem · general topology
IsCompact.image_of_continuousOn
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
IsCompact s → ContinuousOn f s → IsCompact (f '' s)- Defined in
- Mathlib.Topology.Compactness.Compact
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Filterproof · cited by 8,121
- Set.imagestatement and proof · cited by 5,609
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- nhdsWithinproof · cited by 1,912
- ContinuousOnstatement and proof · cited by 1,411
- IsCompactstatement and proof · cited by 1,282
- Filter.NeBotproof · cited by 853
- Filter.principalproof · cited by 740
- Filter.comapproof · cited by 546
Cited by24
Results whose statement or proof uses this declaration.
- IsCompact.imageproof · cited by 105
- IsCompact.exists_isMinOnproof · cited by 15
- IsCompact.exists_bound_of_continuousOnproof · cited by 8
- IsGreatest.norm_cfcproof · cited by 6
- ChartedSpace.locallyCompactSpaceproof · cited by 5
- IsGreatest.norm_cfcₙproof · cited by 5
- NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSetproof · cited by 3
- ContinuousOn.integrableOn_of_subset_isCompactproof · cited by 3
- BoxIntegral.integrable_of_continuousOnproof · cited by 3
- ContinuousOn.image_Iccproof · cited by 3
- SmoothBumpFunction.isCompact_symm_image_closedBallproof · cited by 2
- ContinuousOn.aestronglyMeasurable_of_subset_isCompactproof · cited by 2