Structures · Topology
Topology.IsLower
The lower topology is the topology generated by the complements of the left-closed right-infinite intervals.
- Shape
- One type argument · adds topology_eq_lowerTopology
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Topology.WithLower
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- Topology.IsLower.topology_eq
- Topology.IsLower.isLowerSet_of_isOpen
- Topology.IsLower.isTopologicalBasis
- Topology.IsLower.topology_eq_lowerTopology
- Topology.IsLower.continuous_iff_Ici
- PrimitiveSpectrum.isClosed_iff
- Topology.IsLower.isTopologicalBasis_insert_univ_subbasis
- PrimitiveSpectrum.isTopologicalBasis_relativeLower
- sInfHom.continuous
- Topology.IsLower.isTopologicalSpace_basis
- Topology.IsLower.tendsto_nhds_iff_not_le
- PrimitiveSpectrum.isOpen_iff
- Topology.IsLower.withLowerHomeomorph
- Topology.IsLower.tendsto_nhds_iff_lt
- Topology.IsLower.isClosed_upperClosure
- PrimitiveSpectrum.hull_kernel_of_isClosed
- Topology.IsLower.isUpperSet_of_isClosed
- Topology.IsLower.closure_singleton
- Topology.IsLower.isOpen_iff_generate_Ici_compl
- PrimitiveSpectrum.closedsGC_closureOperator
- Topology.IsLower.toContinuousInf
- Topology.IsLowerSet.lowerSet_le_lower
- Topology.IsLower.t0Space
- Topology.IsLower.instClosedIciTopology
- Topology.instIsLowerProd
- Topology.IsLower.scottHausdorff_le
- OrderDual.instIsUpper
- Topology.IsLowerSet.monotone_to_lowerTopology_continuous
Ancestors0
No ancestors.