Basic

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

Statistics

Metric	Count
Definitions `DiffeologicalSpace`, `CorePlotsOn`, `dTopology`, `isPlot`, `isPlotOn`, `dTopology`, `generateFrom`, `giGenerateFrom`, `instCompleteLattice`, `instPartialOrder`, `mkOfClosure`, `ofCorePlotsOn`, `plots`, `replaceDTopology`, `toPlots`, `DSmooth`, `IsContDiffCompatible`, `IsDTopologyCompatible`, `IsPlot`, `dTopology`, `instDiffeologicalSpaceEuclideanSpaceRealOfFintype`, `instDiffeologicalSpaceReal`, `toDiffeology`	23
Theorems `dSmooth`, `isPlot`, `isOpen_iff_preimages_plots`, `isPlotOn_congr`, `isPlotOn_reparam`, `isPlotOn_univ`, `isPlot_const`, `locality`, `constant_plots`, `ext`, `ext_iff`, `gc_generateFrom`, `generateFrom_iInter_of_generateFrom_eq_self`, `generateFrom_iInter_toPlots`, `generateFrom_iUnion`, `generateFrom_iUnion_toPlots`, `generateFrom_inter_toPlots`, `generateFrom_le_iff`, `generateFrom_le_iff_subset_toPlots`, `generateFrom_mono`, `generateFrom_sUnion`, `generateFrom_surjective`, `generateFrom_toPlots`, `generateFrom_union`, `generateFrom_union_toPlots`, `injective_toPlots`, `isOpen_iff_preimages_plots`, `isPlot_generatedFrom_of_mem`, `isPlot_iInf_iff`, `isPlot_inf_iff`, `isPlot_sInf_iff`, `le_def`, `le_iff`, `le_iff'`, `leftInverse_generateFrom`, `locality`, `mkOfClosure_eq_generateFrom`, `plot_reparam`, `replaceDTopology_eq`, `self_subset_toPlots_generateFrom`, `toPlots_iInf`, `toPlots_inf`, `toPlots_sInf`, `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`	71
Total	94

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`
`generateFrom` 📖	CompOp	18 math math: `leftInverse_generateFrom`, `mkOfClosure_eq_generateFrom`, `generateFrom_le_iff_subset_toPlots`, `generateFrom_iUnion_toPlots`, `generateFrom_le_iff`, `isPlot_generatedFrom_of_mem`, `generateFrom_iInter_of_generateFrom_eq_self`, `generateFrom_union`, `generateFrom_toPlots`, `generateFrom_surjective`, `gc_generateFrom`, `generateFrom_iUnion`, `generateFrom_sUnion`, `generateFrom_iInter_toPlots`, `generateFrom_union_toPlots`, `self_subset_toPlots_generateFrom`, `generateFrom_inter_toPlots`, `generateFrom_mono`
`giGenerateFrom` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	14 math math: `toPlots_sInf`, `generateFrom_iUnion_toPlots`, `generateFrom_iInter_of_generateFrom_eq_self`, `toPlots_iInf`, `isPlot_iInf_iff`, `generateFrom_union`, `isPlot_inf_iff`, `generateFrom_iUnion`, `generateFrom_sUnion`, `generateFrom_iInter_toPlots`, `toPlots_inf`, `generateFrom_union_toPlots`, `generateFrom_inter_toPlots`, `isPlot_sInf_iff`
`instPartialOrder` 📖	CompOp	7 math math: `generateFrom_le_iff_subset_toPlots`, `le_def`, `generateFrom_le_iff`, `le_iff`, `gc_generateFrom`, `le_iff'`, `generateFrom_mono`
`mkOfClosure` 📖	CompOp	1 math math: `mkOfClosure_eq_generateFrom`
`ofCorePlotsOn` 📖	CompOp	—
`plots` 📖	CompOp	4 math math: `locality`, `plot_reparam`, `le_iff`, `constant_plots`
`replaceDTopology` 📖	CompOp	1 math math: `replaceDTopology_eq`
`toPlots` 📖	CompOp	14 math math: `leftInverse_generateFrom`, `toPlots_sInf`, `generateFrom_le_iff_subset_toPlots`, `le_def`, `generateFrom_iUnion_toPlots`, `toPlots_iInf`, `generateFrom_toPlots`, `gc_generateFrom`, `generateFrom_iInter_toPlots`, `toPlots_inf`, `generateFrom_union_toPlots`, `injective_toPlots`, `self_subset_toPlots_generateFrom`, `generateFrom_inter_toPlots`

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`
`gc_generateFrom` 📖	mathematical	—	`GaloisConnection` `Set` `DiffeologicalSpace` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrder` `generateFrom` `toPlots`	—	`generateFrom_le_iff_subset_toPlots`
`generateFrom_iInter_of_generateFrom_eq_self` 📖	mathematical	`toPlots` `generateFrom`	`generateFrom` `Set.iInter` `iInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisInsertion.l_iInf_of_ul_eq_self`
`generateFrom_iInter_toPlots` 📖	mathematical	—	`generateFrom` `Set.iInter` `toPlots` `iInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisInsertion.l_iInf_u`
`generateFrom_iUnion` 📖	mathematical	—	`generateFrom` `Set.iUnion` `iSup` `DiffeologicalSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_generateFrom`
`generateFrom_iUnion_toPlots` 📖	mathematical	—	`generateFrom` `Set.iUnion` `toPlots` `iSup` `DiffeologicalSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisInsertion.l_iSup_u`
`generateFrom_inter_toPlots` 📖	mathematical	—	`generateFrom` `Set` `Set.instInter` `toPlots` `DiffeologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisInsertion.l_inf_u`
`generateFrom_le_iff` 📖	mathematical	—	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `generateFrom` `Diffeology.IsPlot`	—	`generateFrom_le_iff_subset_toPlots`
`generateFrom_le_iff_subset_toPlots` 📖	mathematical	—	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `generateFrom` `Set` `Set.instHasSubset` `toPlots`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `self_subset_toPlots_generateFrom`
`generateFrom_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `generateFrom`	—	`GaloisConnection.monotone_l` `gc_generateFrom`
`generateFrom_sUnion` 📖	mathematical	—	`generateFrom` `Set.sUnion` `iSup` `DiffeologicalSpace` `Set` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `gc_generateFrom`
`generateFrom_surjective` 📖	mathematical	—	`Set` `DiffeologicalSpace` `generateFrom`	—	`GaloisInsertion.l_surjective`
`generateFrom_toPlots` 📖	mathematical	—	`generateFrom` `toPlots`	—	`GaloisInsertion.l_u_eq`
`generateFrom_union` 📖	mathematical	—	`generateFrom` `Set` `Set.instUnion` `DiffeologicalSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_generateFrom`
`generateFrom_union_toPlots` 📖	mathematical	—	`generateFrom` `Set` `Set.instUnion` `toPlots` `DiffeologicalSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisInsertion.l_sup_u`
`injective_toPlots` 📖	mathematical	—	`DiffeologicalSpace` `Set` `toPlots`	—	`ext` `Set.ext_iff`
`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`	—	—
`isPlot_generatedFrom_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Diffeology.IsPlot` `generateFrom`	—	`self_subset_toPlots_generateFrom`
`isPlot_iInf_iff` 📖	mathematical	—	`Diffeology.IsPlot` `iInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`Set.ext_iff` `toPlots_iInf` `Set.mem_iInter`
`isPlot_inf_iff` 📖	mathematical	—	`Diffeology.IsPlot` `DiffeologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`Set.ext_iff` `toPlots_inf`
`isPlot_sInf_iff` 📖	mathematical	—	`Diffeology.IsPlot` `InfSet.sInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`Set.ext_iff` `toPlots_sInf` `Set.mem_iInter₂`
`le_def` 📖	mathematical	—	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instHasSubset` `toPlots`	—	—
`le_iff` 📖	mathematical	—	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instHasSubset` `plots`	—	`le_def`
`le_iff'` 📖	mathematical	—	`DiffeologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Diffeology.IsPlot`	—	`le_iff`
`leftInverse_generateFrom` 📖	mathematical	—	`DiffeologicalSpace` `Set` `generateFrom` `toPlots`	—	`GaloisInsertion.leftInverse_l_u`
`locality` 📖	mathematical	`Set` `EuclideanSpace` `Real` `IsOpen` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.instMembership` `plots`	`Set` `Set.instMembership` `plots`	—	—
`mkOfClosure_eq_generateFrom` 📖	mathematical	`toPlots` `generateFrom`	`mkOfClosure` `generateFrom`	—	`injective_toPlots`
`plot_reparam` 📖	mathematical	`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`	`Set` `Set.instMembership` `plots` `EuclideanSpace` `Real`	—	—
`replaceDTopology_eq` 📖	mathematical	`dTopology`	`replaceDTopology`	—	`ext`
`self_subset_toPlots_generateFrom` 📖	mathematical	—	`Set` `Set.instHasSubset` `toPlots` `generateFrom`	—	—
`toPlots_iInf` 📖	mathematical	—	`toPlots` `iInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter`	—	`GaloisConnection.u_iInf` `gc_generateFrom`
`toPlots_inf` 📖	mathematical	—	`toPlots` `DiffeologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.instInter`	—	—
`toPlots_sInf` 📖	mathematical	—	`toPlots` `InfSet.sInf` `DiffeologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter` `Set` `Set.instMembership`	—	`GaloisConnection.u_sInf` `gc_generateFrom`

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	4 math math: `isPlotOn_reparam`, `isPlotOn_congr`, `locality`, `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` 📖	mathematical	`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` `EuclideanSpace` `Real`	—	—
`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` 📖	mathematical	`IsOpen` `EuclideanSpace` `Real` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership` `isPlotOn`	`isPlotOn`	—	—

Diffeology

Definitions

Name	Category	Theorems
`DSmooth` 📖	MathDef	10 math math: `dSmooth_const`, `IsPlot.dSmooth`, `DSmooth.comp'`, `DSmooth.comp`, `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	19 math math: `isPlot_id'`, `DSmooth.isPlot`, `DiffeologicalSpace.generateFrom_le_iff`, `DiffeologicalSpace.isPlot_generatedFrom_of_mem`, `IsPlot.dSmooth_comp'`, `DiffeologicalSpace.isPlot_iInf_iff`, `isPlot_iff_contDiff`, `isPlot_iff_dSmooth`, `isPlot_reparam`, `IsContDiffCompatible.isPlot_iff`, `DiffeologicalSpace.isPlot_inf_iff`, `isPlot_id`, `DiffeologicalSpace.ext_iff`, `DiffeologicalSpace.le_iff'`, `IsPlot.dSmooth_comp`, `DiffeologicalSpace.isPlot_sInf_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` 📖	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`	`IsPlot` `EuclideanSpace` `Real`	—	`fact_one_le_two_ennreal` `DiffeologicalSpace.plot_reparam`

Diffeology.DSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`Diffeology.DSmooth`	`Diffeology.DSmooth`	—	—
`comp'` 📖	mathematical	`Diffeology.DSmooth`	`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`	`Diffeology.IsPlot` `EuclideanSpace` `Real`	—	—
`dSmooth_comp'` 📖	mathematical	`Diffeology.IsPlot` `Diffeology.DSmooth`	`Diffeology.IsPlot`	—	—

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	24 math math: `DiffeologicalSpace.leftInverse_generateFrom`, `DiffeologicalSpace.toPlots_sInf`, `DiffeologicalSpace.generateFrom_le_iff_subset_toPlots`, `DiffeologicalSpace.le_def`, `DiffeologicalSpace.generateFrom_iUnion_toPlots`, `DiffeologicalSpace.generateFrom_le_iff`, `DiffeologicalSpace.generateFrom_iInter_of_generateFrom_eq_self`, `DiffeologicalSpace.toPlots_iInf`, `DiffeologicalSpace.le_iff`, `DiffeologicalSpace.isPlot_iInf_iff`, `DiffeologicalSpace.generateFrom_union`, `DiffeologicalSpace.generateFrom_surjective`, `DiffeologicalSpace.isPlot_inf_iff`, `DiffeologicalSpace.gc_generateFrom`, `DiffeologicalSpace.generateFrom_iUnion`, `DiffeologicalSpace.generateFrom_sUnion`, `DiffeologicalSpace.generateFrom_iInter_toPlots`, `DiffeologicalSpace.toPlots_inf`, `DiffeologicalSpace.generateFrom_union_toPlots`, `DiffeologicalSpace.le_iff'`, `DiffeologicalSpace.injective_toPlots`, `DiffeologicalSpace.generateFrom_inter_toPlots`, `DiffeologicalSpace.isPlot_sInf_iff`, `DiffeologicalSpace.generateFrom_mono`

---

← Back to Index