Structures · Topology
PreirreducibleSpace
A preirreducible space is one where there is no non-trivial pair of disjoint opens.
- Defined in
- Mathlib.Topology.Irreducible
- Shape
- One type argument · adds isPreirreducible_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
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 by32
- AlgebraicGeometry.Scheme.PartialMap.comp
- PreirreducibleSpace.isPreirreducible_univ
- AlgebraicGeometry.Scheme.RationalMap.comp
- IsOpen.dense
- IsPreirreducible.of_subtype
- AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_left
- AlgebraicGeometry.Scheme.PartialMap.comp_toPartialMap
- nonempty_preirreducible_inter
- AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_right
- AlgebraicGeometry.Scheme.RationalMap.comp_def
- AlgebraicGeometry.Scheme.PartialMap.comp_restrict_left
- Topology.IsOpenEmbedding.preirreducibleSpace
- AlgebraicGeometry.Scheme.PartialMap.comp_restrict_right
- AlgebraicGeometry.Scheme.RationalMap.toRationalMap_comp
- Function.Surjective.preirreducibleSpace
- instExtremallyDisconnectedOfPreirreducibleSpace
- AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv
- AlgebraicGeometry.Scheme.RationalMap.comp.congr_simp
- AlgebraicGeometry.Scheme.RationalMap.instIsDominantComp
- AlgebraicGeometry.Scheme.PartialMap.comp_id
- AlgebraicGeometry.Scheme.PartialMap.comp_domain
- AlgebraicGeometry.Scheme.PartialMap.comp_hom
- not_preirreducible_nontrivial_t2
- AlgebraicGeometry.Scheme.RationalMap.comp_id
- AlgebraicGeometry.Scheme.PartialMap.comp_assoc
- PreirreducibleSpace.preconnectedSpace
- AlgebraicGeometry.Scheme.RationalMap.isOver_comp
- AlgebraicGeometry.Scheme.PartialMap.isDominant_comp_hom
- AlgebraicGeometry.Scheme.RationalMap.comp_assoc
- AlgebraicGeometry.Scheme.PartialMap.comp.congr_simp
- AlgebraicGeometry.Scheme.RationalMap.comp_toRationalMap
- IsOpenMap.denseRange_of_isPreirreducibleSpace
Ancestors0
No ancestors.