Structures · Topology
IsValuativeTopology
We say that a topology on R is valuative if the neighborhoods of 0 in R
are determined by the valuative relation · ≤ᵥ ·.
- Shape
- One type argument · adds mem_nhds_iff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- WithVal
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- Valuation.mem_nhds_iff
- Valuation.isClosed_closedBall
- Valuation.isOpen_closedBall
- Valuation.isClopen_sphere
- Valuation.isOpen_ball
- Valuation.isClopen_closedBall
- Valuation.isClosed_ball
- Valuation.isClopen_ball
- Valuation.isClosed_integer
- IsValuativeTopology.hasBasis_nhds_zero
- IsValuativeTopology.mem_nhds_iff
- Valuation.isOpen_integer
- IsValuativeTopology.hasBasis_nhds
- Valuation.toUniformSpace_eq
- Valuation.mem_nhds_zero_iff
- Valuation.hasBasis_uniformity
- Valuation.isOpen_sphere
- Valuation.hasBasis_nhds_zero
- Valuation.isClopen_integer
- IsValuativeTopology.hasBasis_nhds_zero'
- Valuation.discreteTopology_of_forall_map_eq_one
- Valuation.hasBasis_nhds
- Valuation.is_topological_valuation
- Valuation.isClosed_sphere
- IsValuativeTopology.hasBasis_nhds'
- Valuation.isClopen_valuationSubring
- IsValuativeTopology.v_eq_valuation
- Valuation.isOpen_valuationSubring
- IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup
- IsValuativeTopology.isClopen_sphere
- IsValuativeTopology.isOpen_ball
- Valuation.cauchy_iff
- IsValuativeTopology.isClosed_ball
- IsValuativeTopology.instIsTopologicalAddGroup
- IsValuativeTopology.isClosed_closedBall
- IsValuativeTopology.isClopen_closedBall
- Valuation.discreteTopology_of_forall_lt
- Valuation.locally_const
- IsValuativeTopology.isOpen_sphere
- IsValuativeTopology.isOpen_closedBall
- IsValuativeTopology.continuous_valuation
- IsValuativeTopology.isClopen_ball
- IsValuativeTopology.mem_nhds_zero_iff
- IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV
- Valuation.toTopologicalSpace_eq
- IsValuativeTopology.mem_nhds_iff'
- IsValuativeTopology.isTopologicalRing
- Valuation.isClosed_valuationSubring
Ancestors0
No ancestors.