Structures · Topology
NontrivialTopology
A topological space is nontrivial if it is not the indiscrete topology.
- Defined in
- Mathlib.Topology.Order
- Shape
- One type argument · adds ne_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- LinearIsometry.norm_toContinuousLinearMap
- NormedSpace.sphere_nonempty
- exists_norm_ne_zero
- ContinuousLinearMap.norm_id
- exists_norm_eq
- ContinuousLinearMap.homothety_norm
- LinearIsometry.enorm_toContinuousLinearMap
- LinearIsometry.nnnorm_toContinuousLinearMap
- NontrivialTopology.ne_top
- nnnorm_surjective
- Homeomorph.nontrivialTopology
- Topology.IsInducing.nontrivialTopology
- ContinuousLinearMap.norm_inl
- exists_nnnorm_ne_zero'
- Nontrivial.of_nontrivialTopology
- LinearIsometryEquiv.enorm_toContinuousLinearMap
- ContinuousLinearMap.nnnorm_id
- NormedAddGroupHom.norm_id
- LinearIsometryEquiv.norm_toContinuousLinearMap
- SeparationQuotient.norm_normedMk_eq_one
- LinearIsometryEquiv.nnnorm_toContinuousLinearMap
- range_norm
- ContinuousLinearMap.normOneClass
- exists_norm_ne_zero'
- ContinuousLinearMap.norm_inr
- SeparationQuotient.instNontrivialOfNontrivialTopology
- ContinuousLinearMap.norm_single
- range_nnnorm
- exists_nnnorm_ne_zero
Ancestors0
No ancestors.