Documentation Verification Report

Basic

📁 Source: Mathlib/Geometry/Diffeology/Basic.lean

Statistics

Metric	Count
Definitions `DiffeologicalSpace`, `CorePlotsOn`, `dTopology`, `isPlot`, `isPlotOn`, `dTopology`, `ofCorePlotsOn`, `plots`, `replaceDTopology`, `DSmooth`, `IsContDiffCompatible`, `IsDTopologyCompatible`, `IsPlot`, `dTopology`, `instDiffeologicalSpaceEuclideanSpaceRealOfFintype`, `instDiffeologicalSpaceReal`, `toDiffeology`	17
Theorems `dSmooth`, `isPlot`, `isOpen_iff_preimages_plots`, `isPlotOn_congr`, `isPlotOn_reparam`, `isPlotOn_univ`, `isPlot_const`, `locality`, `constant_plots`, `ext`, `ext_iff`, `isOpen_iff_preimages_plots`, `locality`, `plot_reparam`, `replaceDTopology_eq`, `comp`, `comp'`, `contDiff`, `continuous`, `continuous'`, `isPlot`, `isPlot_iff`, `dTop_eq`, `contDiff`, `continuous`, `dSmooth`, `dSmooth_comp`, `dSmooth_comp'`, `dSmooth_const`, `dSmooth_id`, `dSmooth_id'`, `dSmooth_iff`, `dSmooth_iff_contDiff`, `instIsContDiffCompatible`, `instIsDTopologyCompatible`, `isOpen_iff_preimages_plots`, `isPlot_const`, `isPlot_id`, `isPlot_id'`, `isPlot_iff_contDiff`, `isPlot_iff_dSmooth`, `isPlot_reparam`, `isContDiffCompatible_iff_eq_toDiffeology`	43
Total	60

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dSmooth` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat`	`Diffeology.DSmooth`	—	`isPlot` `comp` `fact_one_le_two_ennreal` `Diffeology.IsPlot.contDiff`
`isPlot` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	`Diffeology.IsPlot`	—	`fact_one_le_two_ennreal` `Diffeology.isPlot_iff_contDiff`

DiffeologicalSpace

Definitions

Name	Category	Theorems
`CorePlotsOn` 📖	CompData	—
`dTopology` 📖	CompOp	1 math math: `isOpen_iff_preimages_plots`
`ofCorePlotsOn` 📖	CompOp	—
`plots` 📖	CompOp	1 math math: `constant_plots`
`replaceDTopology` 📖	CompOp	1 math math: `replaceDTopology_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constant_plots` 📖	mathematical	—	`Set` `Set.instMembership` `plots`	—	—
`ext` 📖	—	`Diffeology.IsPlot`	—	—	`fact_one_le_two_ennreal` `TopologicalSpace.ext`
`ext_iff` 📖	mathematical	—	`Diffeology.IsPlot`	—	`ext`
`isOpen_iff_preimages_plots` 📖	mathematical	—	`TopologicalSpace.IsOpen` `dTopology` `IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.preimage`	—	—
`locality` 📖	—	`IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership` `plots`	—	—	—
`plot_reparam` 📖	—	`Set` `Set.instMembership` `plots` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	—	—
`replaceDTopology_eq` 📖	mathematical	`dTopology`	`replaceDTopology`	—	`ext`

DiffeologicalSpace.CorePlotsOn

Definitions

Name	Category	Theorems
`dTopology` 📖	CompOp	1 math math: `isOpen_iff_preimages_plots`
`isPlot` 📖	MathDef	2 math math: `isPlot_const`, `isPlotOn_univ`
`isPlotOn` 📖	MathDef	2 math math: `isPlotOn_congr`, `isPlotOn_univ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_iff_preimages_plots` 📖	mathematical	—	`TopologicalSpace.IsOpen` `dTopology` `IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.preimage`	—	—
`isPlotOn_congr` 📖	mathematical	`IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.EqOn`	`isPlotOn`	—	—
`isPlotOn_reparam` 📖	—	`IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.MapsTo` `isPlotOn` `ContDiffOn` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	—	—
`isPlotOn_univ` 📖	mathematical	—	`isPlotOn` `Set.univ` `EuclideanSpace` `Real` `isOpen_univ` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `isPlot`	—	—
`isPlot_const` 📖	mathematical	—	`isPlot`	—	—
`locality` 📖	—	`IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership` `isPlotOn`	—	—	—

Diffeology

Definitions

Name	Category	Theorems
`DSmooth` 📖	MathDef	8 math math: `dSmooth_const`, `IsPlot.dSmooth`, `dSmooth_id`, `isPlot_iff_dSmooth`, `ContDiff.dSmooth`, `dSmooth_iff`, `dSmooth_id'`, `dSmooth_iff_contDiff`
`IsContDiffCompatible` 📖	CompData	2 math math: `instIsContDiffCompatible`, `NormedSpace.isContDiffCompatible_iff_eq_toDiffeology`
`IsDTopologyCompatible` 📖	CompData	1 math math: `instIsDTopologyCompatible`
`IsPlot` 📖	MathDef	10 math math: `isPlot_id'`, `DSmooth.isPlot`, `isPlot_iff_contDiff`, `isPlot_iff_dSmooth`, `IsContDiffCompatible.isPlot_iff`, `isPlot_id`, `DiffeologicalSpace.ext_iff`, `ContDiff.isPlot`, `isPlot_const`, `dSmooth_iff`
`dTopology` 📖	CompOp	4 math math: `DSmooth.continuous`, `isOpen_iff_preimages_plots`, `IsPlot.continuous`, `IsDTopologyCompatible.dTop_eq`
`instDiffeologicalSpaceEuclideanSpaceRealOfFintype` 📖	CompOp	4 math math: `isPlot_id'`, `IsPlot.dSmooth`, `isPlot_iff_dSmooth`, `isPlot_id`
`instDiffeologicalSpaceReal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dSmooth_const` 📖	mathematical	—	`DSmooth`	—	`isPlot_const`
`dSmooth_id` 📖	mathematical	—	`DSmooth`	—	`CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`dSmooth_id'` 📖	mathematical	—	`DSmooth`	—	`dSmooth_id`
`dSmooth_iff` 📖	mathematical	—	`DSmooth` `IsPlot` `EuclideanSpace` `Real`	—	—
`dSmooth_iff_contDiff` 📖	mathematical	—	`DSmooth` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	`DSmooth.contDiff` `ContDiff.dSmooth`
`instIsContDiffCompatible` 📖	mathematical	—	`IsContDiffCompatible` `NormedSpace.toDiffeology`	—	—
`instIsDTopologyCompatible` 📖	mathematical	—	`IsDTopologyCompatible` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toDiffeology`	—	—
`isOpen_iff_preimages_plots` 📖	mathematical	—	`IsOpen` `dTopology` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.preimage`	—	`DiffeologicalSpace.isOpen_iff_preimages_plots`
`isPlot_const` 📖	mathematical	—	`IsPlot`	—	`DiffeologicalSpace.constant_plots`
`isPlot_id` 📖	mathematical	—	`IsPlot` `EuclideanSpace` `Real` `instDiffeologicalSpaceEuclideanSpaceRealOfFintype` `Fin.fintype`	—	`contDiff_id` `fact_one_le_two_ennreal`
`isPlot_id'` 📖	mathematical	—	`IsPlot` `EuclideanSpace` `Real` `instDiffeologicalSpaceEuclideanSpaceRealOfFintype` `Fin.fintype`	—	`isPlot_id`
`isPlot_iff_contDiff` 📖	mathematical	—	`IsPlot` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	`IsContDiffCompatible.isPlot_iff`
`isPlot_iff_dSmooth` 📖	mathematical	—	`IsPlot` `DSmooth` `EuclideanSpace` `Real` `instDiffeologicalSpaceEuclideanSpaceRealOfFintype` `Fin.fintype`	—	`IsPlot.dSmooth` `DSmooth.isPlot`
`isPlot_reparam` 📖	—	`IsPlot` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	—	`fact_one_le_two_ennreal` `DiffeologicalSpace.plot_reparam`

Diffeology.DSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Diffeology.DSmooth`	—	—	—
`comp'` 📖	—	`Diffeology.DSmooth`	—	—	`comp`
`contDiff` 📖	mathematical	`Diffeology.DSmooth`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearEquiv.symm_comp_self` `ContDiff.comp` `Diffeology.IsPlot.contDiff` `ContDiff.isPlot` `ContinuousLinearEquiv.contDiff`
`continuous` 📖	mathematical	`Diffeology.DSmooth`	`Continuous` `Diffeology.dTopology`	—	`Diffeology.isOpen_iff_preimages_plots`
`continuous'` 📖	mathematical	`Diffeology.DSmooth`	`Continuous`	—	`Diffeology.IsDTopologyCompatible.dTop_eq` `continuous`
`isPlot` 📖	mathematical	`Diffeology.DSmooth` `EuclideanSpace` `Real` `Diffeology.instDiffeologicalSpaceEuclideanSpaceRealOfFintype` `Fin.fintype`	`Diffeology.IsPlot`	—	`contDiff_id` `fact_one_le_two_ennreal`

Diffeology.IsContDiffCompatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPlot_iff` 📖	mathematical	—	`Diffeology.IsPlot` `ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	—

Diffeology.IsDTopologyCompatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dTop_eq` 📖	mathematical	—	`Diffeology.dTopology`	—	—

Diffeology.IsPlot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	`Diffeology.IsPlot`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `PiLp.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop.some` `ENat` `Top.top` `instTopENat`	—	`fact_one_le_two_ennreal` `Diffeology.isPlot_iff_contDiff`
`continuous` 📖	mathematical	`Diffeology.IsPlot`	`Continuous` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Diffeology.dTopology`	—	`continuous_def` `Diffeology.isOpen_iff_preimages_plots`
`dSmooth` 📖	mathematical	`Diffeology.IsPlot`	`Diffeology.DSmooth` `EuclideanSpace` `Real` `Diffeology.instDiffeologicalSpaceEuclideanSpaceRealOfFintype` `Fin.fintype`	—	`Diffeology.isPlot_reparam`
`dSmooth_comp` 📖	mathematical	`Diffeology.IsPlot` `Diffeology.DSmooth`	`EuclideanSpace` `Real`	—	—
`dSmooth_comp'` 📖	—	`Diffeology.IsPlot` `Diffeology.DSmooth`	—	—	—

NormedSpace

Definitions

Name	Category	Theorems
`toDiffeology` 📖	CompOp	3 math math: `Diffeology.instIsDTopologyCompatible`, `Diffeology.instIsContDiffCompatible`, `isContDiffCompatible_iff_eq_toDiffeology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isContDiffCompatible_iff_eq_toDiffeology` 📖	mathematical	—	`Diffeology.IsContDiffCompatible` `toDiffeology`	—	`DiffeologicalSpace.ext` `Diffeology.IsContDiffCompatible.isPlot_iff` `Diffeology.instIsContDiffCompatible`

(root)

Definitions

Name	Category	Theorems
`DiffeologicalSpace` 📖	CompData	—

---

← Back to Index