GeneratedBy

📁 Source: Mathlib/Topology/Convenient/GeneratedBy.lean

Statistics

Metric	Count
Definitions generatedBy, IsGeneratedBy, homeomorph, WithGeneratedByTopology, equiv, instTopologicalSpace	6
Theorems isGeneratedBy, isGeneratedBy, isGeneratedBy, isGeneratedBy, generatedBy_le, generatedBy_mono, coinduced, continuous_equiv_symm, continuous_iff, equiv_symm_comp_continuous_iff, generatedBy_eq, homeomorph_coe, homeomorph_symm_coe, iSup, iff_le_generatedBy, inst, instPUnit, instWithGeneratedByTopology, isClosed_iff, isOpen_iff, le_generatedBy, sup, isGeneratedBy, continuous_equiv, continuous_from_iff, isClosed_iff, isOpen_iff, isGeneratedBy_iff	28
Total	34

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneratedBy 📖	mathematical	—	Topology.IsGeneratedBy instTopologicalSpaceQuot	—	Topology.IsQuotientMap.isGeneratedBy

Quotient

Theorems

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

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneratedBy 📖	mathematical	Topology.IsGeneratedBy	instTopologicalSpaceSigma	—	Topology.IsGeneratedBy.iSup Topology.IsGeneratedBy.coinduced

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneratedBy 📖	mathematical	—	Topology.IsGeneratedBy instTopologicalSpaceSum	—	Topology.IsGeneratedBy.sup Topology.IsGeneratedBy.coinduced

TopologicalSpace

Definitions

Name	Category	Theorems
generatedBy 📖	CompOp	5 math math: generatedBy_mono, Topology.IsGeneratedBy.le_generatedBy, Topology.IsGeneratedBy.generatedBy_eq, Topology.IsGeneratedBy.iff_le_generatedBy, generatedBy_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generatedBy_le 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder generatedBy	—	Continuous.isOpen_preimage Topology.WithGeneratedByTopology.continuous_equiv
generatedBy_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder	generatedBy	—	iSup₂_le le_iSup₂_of_le continuous_le_rng ContinuousMap.continuous_toFun le_rfl

Topology

Definitions

Name	Category	Theorems
IsGeneratedBy 📖	CompData	11 math math: Sum.isGeneratedBy, IsGeneratedBy.instWithGeneratedByTopology, IsGeneratedBy.coinduced, IsGeneratedBy.iff_le_generatedBy, isGeneratedBy_iff, Quotient.isGeneratedBy, IsGeneratedBy.sup, Quot.isGeneratedBy, IsQuotientMap.isGeneratedBy, IsGeneratedBy.inst, IsGeneratedBy.instPUnit
WithGeneratedByTopology 📖	CompOp	10 math math: IsGeneratedBy.homeomorph_symm_coe, IsGeneratedBy.instWithGeneratedByTopology, isGeneratedBy_iff, IsGeneratedBy.continuous_equiv_symm, IsGeneratedBy.equiv_symm_comp_continuous_iff, IsGeneratedBy.homeomorph_coe, WithGeneratedByTopology.continuous_from_iff, WithGeneratedByTopology.isOpen_iff, WithGeneratedByTopology.continuous_equiv, WithGeneratedByTopology.isClosed_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneratedBy_iff 📖	mathematical	—	IsGeneratedBy Continuous WithGeneratedByTopology WithGeneratedByTopology.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm WithGeneratedByTopology.equiv	—	—

Topology.IsGeneratedBy

Definitions

Name	Category	Theorems
homeomorph 📖	CompOp	2 math math: homeomorph_symm_coe, homeomorph_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced 📖	mathematical	—	Topology.IsGeneratedBy TopologicalSpace.coinduced	—	iff_le_generatedBy Continuous.coinduced_le equiv_symm_comp_continuous_iff continuous_coinduced_rng
continuous_equiv_symm 📖	mathematical	—	Continuous Topology.WithGeneratedByTopology Topology.WithGeneratedByTopology.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Topology.WithGeneratedByTopology.equiv	—	—
continuous_iff 📖	mathematical	—	Continuous DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	Topology.IsQuotientMap.continuous_iff Homeomorph.isQuotientMap Topology.WithGeneratedByTopology.continuous_from_iff Function.comp_assoc Equiv.self_comp_symm
equiv_symm_comp_continuous_iff 📖	mathematical	—	Continuous Topology.WithGeneratedByTopology Topology.WithGeneratedByTopology.instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Topology.WithGeneratedByTopology.equiv	—	Continuous.comp Topology.WithGeneratedByTopology.continuous_equiv continuous_iff continuous_def Topology.WithGeneratedByTopology.isOpen_iff
generatedBy_eq 📖	mathematical	—	TopologicalSpace.generatedBy	—	le_antisymm TopologicalSpace.generatedBy_le le_generatedBy
homeomorph_coe 📖	mathematical	—	DFunLike.coe Homeomorph Topology.WithGeneratedByTopology Topology.WithGeneratedByTopology.instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph Equiv Equiv.instEquivLike Topology.WithGeneratedByTopology.equiv	—	—
homeomorph_symm_coe 📖	mathematical	—	DFunLike.coe Homeomorph Topology.WithGeneratedByTopology Topology.WithGeneratedByTopology.instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeomorph Equiv Equiv.instEquivLike Equiv.symm Topology.WithGeneratedByTopology.equiv	—	—
iSup 📖	mathematical	Topology.IsGeneratedBy	iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	iff_le_generatedBy iSup_le_iff LE.le.trans le_generatedBy TopologicalSpace.generatedBy_mono le_iSup
iff_le_generatedBy 📖	mathematical	—	Topology.IsGeneratedBy TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.generatedBy	—	le_generatedBy continuous_def
inst 📖	mathematical	—	Topology.IsGeneratedBy	—	continuous_def Topology.WithGeneratedByTopology.isOpen_iff continuous_id
instPUnit 📖	mathematical	—	Topology.IsGeneratedBy instTopologicalSpacePUnit	—	iff_le_generatedBy Eq.le Unique.instSubsingleton
instWithGeneratedByTopology 📖	mathematical	—	Topology.IsGeneratedBy Topology.WithGeneratedByTopology Topology.WithGeneratedByTopology.instTopologicalSpace	—	continuous_def Topology.WithGeneratedByTopology.isOpen_iff continuous_iff inst Function.comp_assoc equiv_symm_comp_continuous_iff Continuous.comp' ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass
isClosed_iff 📖	mathematical	—	IsClosed Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	Topology.IsQuotientMap.isClosed_preimage Homeomorph.isQuotientMap Equiv.symm_preimage_preimage
isOpen_iff 📖	mathematical	—	IsOpen Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	Topology.IsQuotientMap.isOpen_preimage Homeomorph.isQuotientMap Equiv.symm_preimage_preimage
le_generatedBy 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.generatedBy	—	Continuous.isOpen_preimage continuous_equiv_symm
sup 📖	mathematical	—	Topology.IsGeneratedBy TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sup_eq_iSup iSup

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGeneratedBy 📖	mathematical	Topology.IsQuotientMap	Topology.IsGeneratedBy	—	Topology.IsGeneratedBy.coinduced eq_coinduced

Topology.WithGeneratedByTopology

Definitions

Name	Category	Theorems
equiv 📖	CompOp	9 math math: Topology.IsGeneratedBy.homeomorph_symm_coe, Topology.isGeneratedBy_iff, Topology.IsGeneratedBy.continuous_equiv_symm, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.IsGeneratedBy.homeomorph_coe, continuous_from_iff, isOpen_iff, continuous_equiv, isClosed_iff
instTopologicalSpace 📖	CompOp	10 math math: Topology.IsGeneratedBy.homeomorph_symm_coe, Topology.IsGeneratedBy.instWithGeneratedByTopology, Topology.isGeneratedBy_iff, Topology.IsGeneratedBy.continuous_equiv_symm, Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff, Topology.IsGeneratedBy.homeomorph_coe, continuous_from_iff, isOpen_iff, continuous_equiv, isClosed_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_equiv 📖	mathematical	—	Continuous Topology.WithGeneratedByTopology instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equiv	—	continuous_def isOpen_iff Continuous.isOpen_preimage ContinuousMap.continuous
continuous_from_iff 📖	mathematical	—	Continuous Topology.WithGeneratedByTopology instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv ContinuousMap ContinuousMap.instFunLike	—	continuous_coinduced_dom
isClosed_iff 📖	mathematical	—	IsClosed Topology.WithGeneratedByTopology instTopologicalSpace Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv	—	—
isOpen_iff 📖	mathematical	—	IsOpen Topology.WithGeneratedByTopology instTopologicalSpace Set.preimage DFunLike.coe ContinuousMap ContinuousMap.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equiv	—	—

---

← Back to Index