Structures · Topology
PreconnectedSpace
A preconnected space is one where there is no non-trivial open partition.
- Defined in
- Mathlib.Topology.Connected.Basic
- Shape
- One type argument · adds isPreconnected_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- TopologicalSpace.NonemptyCompacts
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- PreconnectedSpace.isPreconnected_univ
- isClopen_iff
- intermediate_value_univ₂
- IsClopen.eq_univ
- AddTorsor.connectedSpace
- IsSeparatedMap.eq_of_comp_eq
- IsSeparatedMap.const_of_comp
- mem_range_of_exists_le_of_exists_ge
- PreconnectedSpace.trivial_of_discrete
- nonempty_inter
- subsingleton_of_disjoint_isClopen
- IsLocallyConstant.apply_eq_of_preconnectedSpace
- IsLocallyConstant.eq_const
- PreconnectedSpace.induction₂'
- IsCoveringMap.liftHomotopyRel
- isPreconnected_range
- subsingleton_of_preconnected_totallyDisconnected
- IsLocallyConstant.exists_eq_const
- intermediate_value_univ₂_eventually₁
- intermediate_value_univ
- PreconnectedSpace.connectedComponent_eq_univ
- AnalyticOnNhd.eq_of_eventuallyEq
- eq_of_germ_isConstant
- LocallyConstant.apply_eq_of_preconnectedSpace
- IsCoveringMap.eq_of_comp_eq
- NormedAddCommGroup.exists_norm_nsmul_le
- LocallyConstant.eq_const
- DenseRange.preconnectedSpace
- subsingleton_of_disjoint_isClosed_iUnion_eq_univ
- IsCoveringMap.homotopicRel_iff_comp
- intermediate_value_univ₂_eventually₂
- denselyOrdered_of_preconnectedSpace
- subsingleton_of_disjoint_isOpen_iUnion_eq_univ
- LocallyConstant.exists_eq_const
- instPreconnectedSpaceForall
- MDifferentiable.exists_eq_const_of_compactSpace
- PreconnectedSpace.infinite
- IsCoveringMap.const_of_comp
- frontier_eq_empty_iff
- OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace
- AnalyticOnNhd.analyticOrderAt_eq_top_iff_eq_zero
- Pi.locallyConnectedSpace
- instPreconnectedSpaceProd
- ExtremallyDisconnected.toPreirreducibleSpace
- TopologicalSpace.NonemptyCompacts.instPreconnectedSpace
- ConnectedComponents.subsingleton
- PreconnectedSpace.induction₂
- MDifferentiable.apply_eq_of_compactSpace
- nonempty_frontier_iff
- IsDenseInducing.preconnectedSpace
Ancestors0
No ancestors.