Theorems · Definition · global analysis
Diffeology.dTopology
{X : Type u_1} → [self : DiffeologicalSpace X] → TopologicalSpace XAlias of DiffeologicalSpace.dTopology.
The D-topology of the diffeology. This is included as part of the data in order to give
control over what the D-topology is defeq to. See also note [forgetful inheritance].
- Defined in
- Mathlib.Geometry.Diffeology.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- DiffeologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- DiffeologicalSpacestatement · cited by 60
- DiffeologicalSpace.dTopologyproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- Diffeology.isOpen_iff_preimages_plotsstatement · cited by 2
- Diffeology.IsDTopologyCompatible.dTop_eqstatement · cited by 1
- Diffeology.DSmooth.continuousstatement · cited by 1
- Diffeology.IsDTopologyCompatible.casesOnstatement and proof · cited by 0
- Diffeology.IsDTopologyCompatible.recOnstatement and proof · cited by 0
- Diffeology.IsPlot.continuousstatement · cited by 0
- Diffeology.DSmooth.continuous'proof · cited by 0