Theorems · Theorem · general topology
ContinuousMap.continuous_postcomp
∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Continuous g.compC(X, ·) is a functor.
- Defined in
- Mathlib.Topology.CompactOpen
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Continuousstatement · cited by 2,592
- ContinuousMapstatement and proof · cited by 2,491
- IsOpenproof · cited by 2,400
- IsCompactproof · cited by 1,282
- ContinuousMap.compstatement · cited by 181
- IsOpen.preimageproof · cited by 147
- ContinuousMap.continuous_toFunproof · cited by 47
- ContinuousMap.isOpen_setOfPred_mapsToproof · cited by 9
- ContinuousMap.continuous_compactOpenproof · cited by 2
Cited by9
Results whose statement or proof uses this declaration.
- SpectrumRestricts.continuous_starAlgHomproof · cited by 2
- ContinuousMap.continuous_toNNRealproof · cited by 1
- ContinuousMapZero.continuous_postcompproof · cited by 1
- ContinuousMapZero.continuous_toNNRealproof · cited by 1
- ContinuousMap.continuous_rclikeToRealproof · cited by 0
- ContinuousMap.continuous_realToRCLikeproof · cited by 0
- GenLoop.continuous_fromLoopproof · cited by 0
- ContinuousAddMonoidHom.continuous_comp_rightproof · cited by 0
- ContinuousMonoidHom.continuous_comp_rightproof · cited by 0