DeltaGeneratedSpace

📁 Source: Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean

Statistics

Metric	Count
Definitions DeltaGeneratedSpace, counit, instTopologicalSpaceOf, of, deltaGenerated	5
Theorems coinduced, continuous_counit, continuous_iff, iSup, instLocPathConnectedSpace, instOf, instSequentialSpace, isOpen_iff, le_deltaGenerated, sup, deltaGeneratedSpace, deltaGeneratedSpace, deltaGeneratedSpace, deltaGeneratedSpace, deltaGeneratedSpace, continuous_to_deltaGenerated, deltaGeneratedSpace_deltaGenerated, deltaGenerated_deltaGenerated_eq, deltaGenerated_eq_coinduced, deltaGenerated_le, deltaGenerated_mono, eq_deltaGenerated, isOpen_deltaGenerated_iff	23
Total	28

DeltaGeneratedSpace

Definitions

Name	Category	Theorems
counit 📖	CompOp	1 math math: continuous_counit
instTopologicalSpaceOf 📖	CompOp	3 math math: DeltaGenerated.topToDeltaGenerated_map_hom_hom_apply, continuous_counit, instOf
of 📖	CompOp	4 math math: DeltaGenerated.topToDeltaGenerated_map_hom_hom_apply, continuous_counit, instOf, DeltaGenerated.topToDeltaGenerated_obj_toTop_carrier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced 📖	mathematical	—	DeltaGeneratedSpace TopologicalSpace.coinduced	—	Continuous.coinduced_le continuous_to_deltaGenerated continuous_coinduced_rng
continuous_counit 📖	mathematical	—	Continuous of instTopologicalSpaceOf counit	—	continuous_iff_coinduced_le deltaGenerated_le
continuous_iff 📖	mathematical	—	Continuous Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	eq_deltaGenerated TopologicalSpace.deltaGenerated.eq_1 coinduced_iSup coinduced_compose
iSup 📖	mathematical	DeltaGeneratedSpace	iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	iSup_le_iff LE.le.trans le_deltaGenerated deltaGenerated_mono le_iSup
instLocPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace	—	eq_deltaGenerated deltaGenerated_eq_coinduced LocPathConnectedSpace.coinduced Sigma.locPathConnectedSpace LocallyConvexSpace.toLocPathConnectedSpace Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NormedSpace.toLocallyConvexSpace
instOf 📖	mathematical	—	DeltaGeneratedSpace of instTopologicalSpaceOf	—	deltaGeneratedSpace_deltaGenerated
instSequentialSpace 📖	mathematical	—	SequentialSpace	—	eq_deltaGenerated SequentialSpace.iSup SequentialSpace.coinduced FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.instFirstCountableTopologyForallOfCountable instCountableFin TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace
isOpen_iff 📖	mathematical	—	IsOpen Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	eq_deltaGenerated isOpen_deltaGenerated_iff
le_deltaGenerated 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.deltaGenerated	—	—
sup 📖	mathematical	—	DeltaGeneratedSpace TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sup_eq_iSup iSup

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deltaGeneratedSpace 📖	mathematical	—	DeltaGeneratedSpace instTopologicalSpaceQuot	—	Topology.IsQuotientMap.deltaGeneratedSpace

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deltaGeneratedSpace 📖	mathematical	—	DeltaGeneratedSpace instTopologicalSpaceQuotient	—	Topology.IsQuotientMap.deltaGeneratedSpace isQuotientMap_quotient_mk'

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deltaGeneratedSpace 📖	mathematical	DeltaGeneratedSpace	instTopologicalSpaceSigma	—	DeltaGeneratedSpace.iSup DeltaGeneratedSpace.coinduced

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deltaGeneratedSpace 📖	mathematical	—	DeltaGeneratedSpace instTopologicalSpaceSum	—	DeltaGeneratedSpace.sup DeltaGeneratedSpace.coinduced

TopologicalSpace

Definitions

Name	Category	Theorems
deltaGenerated 📖	CompOp	9 math math: deltaGenerated_eq_coinduced, deltaGenerated_le, continuous_to_deltaGenerated, deltaGeneratedSpace_deltaGenerated, DeltaGeneratedSpace.le_deltaGenerated, isOpen_deltaGenerated_iff, deltaGenerated_mono, deltaGenerated_deltaGenerated_eq, eq_deltaGenerated

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deltaGeneratedSpace 📖	mathematical	Topology.IsQuotientMap	DeltaGeneratedSpace	—	DeltaGeneratedSpace.coinduced eq_coinduced

(root)

Definitions

Name	Category	Theorems
DeltaGeneratedSpace 📖	CompData	9 math math: Sum.deltaGeneratedSpace, deltaGeneratedSpace_deltaGenerated, DeltaGeneratedSpace.sup, Quotient.deltaGeneratedSpace, DeltaGeneratedSpace.coinduced, Quot.deltaGeneratedSpace, Topology.IsQuotientMap.deltaGeneratedSpace, DeltaGeneratedSpace.instOf, DeltaGenerated.deltaGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_to_deltaGenerated 📖	mathematical	—	Continuous TopologicalSpace.deltaGenerated	—	—
deltaGeneratedSpace_deltaGenerated 📖	mathematical	—	DeltaGeneratedSpace TopologicalSpace.deltaGenerated	—	deltaGenerated_deltaGenerated_eq le_refl
deltaGenerated_deltaGenerated_eq 📖	mathematical	—	TopologicalSpace.deltaGenerated	—	TopologicalSpace.ext ContinuousMap.continuous_toFun
deltaGenerated_eq_coinduced 📖	mathematical	—	TopologicalSpace.deltaGenerated TopologicalSpace.coinduced ContinuousMap Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap.instFunLike TopologicalSpace instTopologicalSpaceSigma	—	TopologicalSpace.deltaGenerated.eq_1 instTopologicalSpaceSigma.eq_1 coinduced_iSup
deltaGenerated_le 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.deltaGenerated	—	iSup_le_iff Continuous.coinduced_le ContinuousMap.continuous
deltaGenerated_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	TopologicalSpace.deltaGenerated	—	continuous_id_iff_le continuous_to_deltaGenerated deltaGeneratedSpace_deltaGenerated LE.le.trans deltaGenerated_le
eq_deltaGenerated 📖	mathematical	—	TopologicalSpace.deltaGenerated	—	eq_of_le_of_ge DeltaGeneratedSpace.le_deltaGenerated deltaGenerated_le
isOpen_deltaGenerated_iff 📖	mathematical	—	IsOpen TopologicalSpace.deltaGenerated Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	—

---

← Back to Index