Structures · Topology
Topology.IsGeneratedBy
Given a family of topological spaces X i, we say that a topological space is
X-generated (IsGeneratedBy X Y) when the topology on Y is the X-generated
topology, i.e. when the identity is a homeomorphism
WithGeneratedByTopology X Y ≃ₜ Y (see IsGeneratedBy.homeomorph).
- Defined in
- Mathlib.Topology.Convenient.GeneratedBy
- Shape
- 2 explicit arguments · adds continuous_equiv_symm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- Topology.IsGeneratedBy.homeomorph
- Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff
- Topology.IsGeneratedBy.continuous_iff
- Topology.IsGeneratedBy.le_generatedBy
- Topology.IsQuotientMap.isGeneratedBy
- Topology.IsGeneratedBy.coinduced
- Topology.IsGeneratedBy.isOpen_iff
- Topology.ContinuousMapGeneratedBy.curryEquiv
- Topology.IsGeneratedBy.generatedBy_eq
- Topology.ContinuousMapGeneratedBy.ev
- Topology.ContinuousMapGeneratedBy.postcomp
- IsOpen.isGeneratedBy
- IsClosed.isGeneratedBy
- Topology.IsGeneratedBy.continuous_equiv_symm
- Topology.IsGeneratedBy.isClosed_iff
- Sigma.deltaGeneratedSpace
- DeltaGeneratedSpace.continuous_iff
- Quot.deltaGeneratedSpace
- Topology.IsGeneratedBy.homeomorph_symm_coe
- Topology.ContinuousMapGeneratedBy.curryEquiv_apply_apply
- Topology.ContinuousMapGeneratedBy.postcomp_apply
- Quotient.deltaGeneratedSpace
- Quot.isGeneratedBy
- GeneratedByTopCat.of
- DeltaGeneratedSpace.isOpen_iff
- Sum.isGeneratedBy
- Sigma.isGeneratedBy
- eq_deltaGenerated
- Topology.IsQuotientMap.deltaGeneratedSpace
- DeltaGeneratedSpace.coinduced
- Sum.deltaGeneratedSpace
- Quotient.isGeneratedBy
- Topology.ContinuousMapGeneratedBy.curryEquiv_symm_apply
- Topology.IsClosedEmbedding.isGeneratedBy
- Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_dom_prod_iff
- Topology.ContinuousMapGeneratedBy.ev_apply
- Topology.IsOpenEmbedding.isGeneratedBy
- Topology.IsGeneratedBy.homeomorph_coe
- Topology.IsGeneratedBy.homeomorph.congr_simp
Ancestors0
No ancestors.