Structures · Topology
Topology.IsUpper
The upper topology is the topology generated by the complements of the right-closed left-infinite intervals.
- Shape
- One type argument · adds topology_eq_upperTopology
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Topology.WithUpper
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- Topology.IsUpper.isUpperSet_of_isOpen
- Topology.IsUpper.isTopologicalSpace_basis
- Topology.IsUpper.topology_eq
- Topology.IsUpper.topology_eq_upperTopology
- Topology.IsUpperSet.monotone_to_upperTopology_continuous
- OrderDual.instIsLower
- Topology.IsUpper.toContinuousInf
- Topology.IsUpperSet.upperSet_le_upper
- Topology.IsUpper.withUpperHomeomorph
- Topology.IsUpper.isOpen_iff_generate_Iic_compl
- Topology.IsScott.instUnivSetOfIsUpper
- sSupHom.continuous
- Topology.IsUpper.continuous_iff_Iic
- Topology.IsUpper.t0Space
- Topology.IsUpper.isTopologicalBasis
- Topology.IsUpper.tendsto_nhds_iff_not_le
- Topology.IsUpper.instClosedIicTopology
- Topology.IsUpper.closure_singleton
- Topology.IsUpper.tendsto_nhds_iff_lt
- Topology.instIsUpperProd
- Topology.IsUpper.isLowerSet_of_isClosed
- Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis
- Topology.IsUpper.isClosed_lowerClosure
Ancestors0
No ancestors.