Theorems · Theorem · general topology
Topology.ContinuousMapGeneratedBy.continuous_precomp
∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Z : Type v'} [inst_1 : TopologicalSpace Z]
{T : Type v''} [inst_2 : TopologicalSpace T] {i : ι} (f : C(X i, Z)),
Continuous (Topology.ContinuousMapGeneratedBy.precomp f)- Defined in
- Mathlib.Topology.Convenient.HomSpace
- Cited by
- 0 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.
Cites10
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
- LE.le.transproof · cited by 3,151
- Continuousstatement · cited by 2,592
- ContinuousMapstatement and proof · cited by 2,491
- iInfproof · cited by 1,690
- TopologicalSpace.inducedproof · cited by 148
- iInf_leproof · cited by 104
- Topology.ContinuousMapGeneratedBystatement · cited by 28
- continuous_iff_le_inducedproof · cited by 16
- Topology.ContinuousMapGeneratedBy.precompstatement and proof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.