instValuedValueGroupWithZeroOfIsUniformAddGroup

English

For any x, the neighborhood filter 𝓝 x has a basis consisting of sets { z | v(z − x) < γ } parameterized by γ ∈ (ValueGroupWithZero R)×.

Русский

Для любого x фильтр окрестностей 𝓝 x имеет базис, состоящий из множеств { z | v(z − x) < γ } с параметрами γ ∈ (ValueGroupWithZero R)×.

LaTeX

$$$(\\mathcal{N}_x) \\text{ has basis } (\\gamma \mapsto \\{ z \\in R \\mid v(z - x) < \\gamma \\})$$$

Lean4

/-- Helper `Valued` instance when `ValuativeTopology R` over a `UniformSpace R`,
for use in porting files from `Valued` to `ValuativeRel`. -/
instance (priority := low) {R : Type*} [CommRing R] [ValuativeRel R] [UniformSpace R] [IsUniformAddGroup R]
    [IsValuativeTopology R] : Valued R (ValueGroupWithZero R)
    where
  «v» := valuation R
  is_topological_valuation := mem_nhds_zero_iff

Похожие утверждения