Theorems · Theorem · general topology
TopologicalSpace.PositiveCompacts.map_id
∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.PositiveCompacts α),
TopologicalSpace.PositiveCompacts.map id ⋯ ⋯ K = K- Defined in
- Mathlib.Topology.Sets.Compacts
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- continuous_idstatement · cited by 192
- TopologicalSpace.PositiveCompactsstatement and proof · cited by 112
- Set.image_idproof · cited by 60
- TopologicalSpace.Compacts.carrierproof · cited by 45
- TopologicalSpace.PositiveCompacts.toCompactsproof · cited by 14
- IsOpenMap.idstatement · cited by 12
- TopologicalSpace.PositiveCompacts.mapstatement · cited by 7
- TopologicalSpace.PositiveCompacts.extproof · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.