The topology on a ring induced by a valuation

In this file, we define the non-Archimedean topology induced by a valuation on a ring.

Main definitions

• If we have both [ValuativeRel R] and [TopologicalSpace R], then writing [IsValuativeTopology R] ensures that the topology on R agrees with the one induced by the valuation.
• ValuativeRel.uniformSpace: The uniform structure introduced by a ValuativeRel.

NOTE (2026-03-17): The Valued instance on a ring R would be replaced by [ValuativeRel R] [UniformSpace R] [IsValuativeTopology R] [IsUniformAddGroup R] (or [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] when the uniformity is not relevant). Additional input (v : Valuation R Γ₀) [v.Compatible] can be introduced whenever a specific compatible valuation is chosen.

The canonical way to introduce the topological structure from a chosen valuation is:

1. First define the ValuativeRel structure using ValuativeRel.ofValuation;
2. Then define the UniformSpace structure using ValuativeRel.uniformSpace.

theorem Valuation.exists_setOf_restrict_le_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] (x : R) (s : Set R) : (∃ (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ), {z : R | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {a : R | (ValuativeRel.valuation R) (a - x) < ↑γ} ⊆ s

class IsValuativeTopology (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] : Prop

We say that a topology on R is valuative if the neighborhoods of 0 in R are determined by the valuative relation · ≤ᵥ ·.

• mem_nhds_iff {s : Set R} {x : R} : s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), (fun (x_1 : R) => x + x_1) '' {z : R | (ValuativeRel.valuation R) z < ↑γ} ⊆ s

@[implicit_reducible]

noncomputable def ValuativeRel.topologicalSpace (R : Type u_1) [CommRing R] [ValuativeRel R] : TopologicalSpace R

The topology induced by a valuative relation. Note that this is not made into a global instance to avoid diamonds. If desired, one can equip a ring with a topological space from a valuative relation by hand. But as long as they do so, the fact that the topology is valuative and nonarchemidean can be automatically inferred.

Equations

• ValuativeRel.topologicalSpace R = ⋯.topology

instance ValuativeRel.nonarchimedeanRing (R : Type u_1) [CommRing R] [ValuativeRel R] : NonarchimedeanRing R

instance ValuativeRel.isValuativeTopology (R : Type u_1) [CommRing R] [ValuativeRel R] : IsValuativeTopology R

@[implicit_reducible]

noncomputable def ValuativeRel.uniformSpace (R : Type u_1) [CommRing R] [ValuativeRel R] : UniformSpace R

The uniform structure induced by a valuative relation. Note that this is not made into a global instance to avoid diamonds. If desired, one can equip a ring with a uniform space from a valuative relation by hand. But as long as they do so, the fact that the topology is valuative and nonarchimedean, and the addition is uniformly continuous, can be automatically inferred.

Equations

• ValuativeRel.uniformSpace R = IsTopologicalAddGroup.rightUniformSpace R

instance ValuativeRel.isUniformAddGroup (R : Type u_1) [CommRing R] [ValuativeRel R] : IsUniformAddGroup R

theorem IsValuativeTopology.mem_nhds_iff' {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] {s : Set R} {x : R} : s ∈ nhds x ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {z : R | (ValuativeRel.valuation R) (z - x) < ↑γ} ⊆ s

A variant of IsValuativeTopology.mem_nhds_iff using subtraction.

theorem IsValuativeTopology.mem_nhds_zero_iff {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (s : Set R) : s ∈ nhds 0 ↔ ∃ (γ : (ValuativeRel.ValueGroupWithZero R)ˣ), {x : R | (ValuativeRel.valuation R) x < ↑γ} ⊆ s

theorem IsValuativeTopology.hasBasis_nhds {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (x : R) : (nhds x).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {z : R | (ValuativeRel.valuation R) (z - x) < ↑γ}

theorem IsValuativeTopology.hasBasis_nhds' {R : Type u_1} [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] (x : R) : (nhds x).HasBasis (fun (x : ValuativeRel.ValueGroupWithZero R) => x ≠ 0) fun (x_1 : ValuativeRel.ValueGroupWithZero R) => {y : R | (ValuativeRel.valuation R) (y - x) < x_1}

A variant of hasBasis_nhds where · ≠ 0 is unbundled.

theorem IsValuativeTopology.hasBasis_nhds_zero (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] : (nhds 0).HasBasis (fun (x : (ValuativeRel.ValueGroupWithZero R)ˣ) => True) fun (γ : (ValuativeRel.ValueGroupWithZero R)ˣ) => {x : R | (ValuativeRel.valuation R) x < ↑γ}

theorem IsValuativeTopology.hasBasis_nhds_zero' (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] : (nhds 0).HasBasis (fun (x : ValuativeRel.ValueGroupWithZero R) => x ≠ 0) fun (x : ValuativeRel.ValueGroupWithZero R) => {x_1 : R | (ValuativeRel.valuation R) x_1 < x}

A variant of hasBasis_nhds_zero where · ≠ 0 is unbundled.

theorem Valuation.mem_nhds_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] {s : Set R} {x : R} : s ∈ nhds x ↔ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ), {z : R | v.restrict (z - x) < ↑γ} ⊆ s

theorem Valuation.mem_nhds_zero_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] (s : Set R) : s ∈ nhds 0 ↔ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ), {x : R | v.restrict x < ↑γ} ⊆ s

theorem Valuation.is_topological_valuation {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] (s : Set R) : s ∈ nhds 0 ↔ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ), {x : R | v.restrict x < ↑γ} ⊆ s

Alias of Valuation.mem_nhds_zero_iff.

theorem Valuation.hasBasis_nhds {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] (x : R) : (nhds x).HasBasis (fun (x : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => True) fun (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => {z : R | v.restrict (z - x) < ↑γ}

theorem Valuation.hasBasis_nhds_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] : (nhds 0).HasBasis (fun (x : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => True) fun (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => {x : R | v.restrict x < ↑γ}

theorem Valuation.locally_const {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] {x : R} (h : v x ≠ 0) : {y : R | v y = v x} ∈ nhds x

The set { y : R | v y = v x } is a neighbourhood of x. This does not imply that v is locally constant everywhere (since v ⁻¹' {0} is not open), but it is equivalent to the restriction of v to the complement of its support being locally constant.

@[instance 100]

instance IsValuativeTopology.instIsTopologicalAddGroup (R : Type u_1) [CommRing R] [ValuativeRel R] [TopologicalSpace R] [IsValuativeTopology R] : IsTopologicalAddGroup R

theorem Valuation.hasBasis_uniformity {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] : (uniformity R).HasBasis (fun (x : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => True) fun (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ) => {p : R × R | v.restrict (p.2 - p.1) < ↑γ}

theorem Valuation.toUniformSpace_eq {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] : _u = IsTopologicalAddGroup.rightUniformSpace R

theorem Valuation.cauchy_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] {F : Filter R} : Cauchy F ↔ F.NeBot ∧ ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ v)ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

theorem Valuation.toTopologicalSpace_eq {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] : _t = ⋯.topology

@[instance 100]

instance IsValuativeTopology.isTopologicalRing {R : Type u_1} [CommRing R] [ValuativeRel R] [_t : TopologicalSpace R] [IsValuativeTopology R] : IsTopologicalRing R

theorem Valuation.discreteTopology_of_forall_map_eq_one {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible] (h : ∀ (x : R), x ≠ 0 → v x = 1) : DiscreteTopology R

theorem Valuation.discreteTopology_of_forall_lt {K : Type u_2} [Field K] [ValuativeRel K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace K] [IsValuativeTopology K] [MulArchimedean Γ₀] (v : Valuation K Γ₀) [v.Compatible] {r : Γ₀} (hr : r ≠ 0) (h : ∀ (x : K), v x ≠ 0 → r < v x) : DiscreteTopology K

theorem Valuation.isOpen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsOpen {x : R | v.restrict x < r}

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is open in the valuative topology.

theorem Valuation.isClosed_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClosed {x : R | v.restrict x < r}

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is closed in the valuative topology.

theorem Valuation.isClopen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClopen {x : R | v.restrict x < r}

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is clopen in the valuative topology.

theorem Valuation.isOpen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsOpen {x : R | v.restrict x ≤ r}

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is open in the valuative topology.

theorem Valuation.isClosed_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClosed {x : R | v.restrict x ≤ r}

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is closed in the valuative topology.

theorem Valuation.isClopen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsClopen {x : R | v.restrict x ≤ r}

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is clopen in the valuative topology.

theorem Valuation.isClopen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsClopen {x : R | v.restrict x = r}

For any valuation v compatible with the valuative relation on R, the sphere of radius r around zero {x | v.restrict x = r} is clopen in the valuative topology.

theorem Valuation.isOpen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsOpen {x : R | v.restrict x = r}

For any valuation v compatible with the valuative relation on R, the sphere of radius r around zero {x | v.restrict x = r} is open in the valuative topology.

theorem Valuation.isClosed_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClosed {x : R | v.restrict x = r}

For any valuation v compatible with the valuative relation on R, the sphere of radius r around zero {x | v.restrict x = r} is closed in the valuative topology.

theorem Valuation.isOpen_integer {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] : IsOpen ↑v.integer

For any valuation v compatible with the valuative relation on R, the closed unit ball around zero {x | v x ≤ 1} is open in the valuative topology.

theorem Valuation.isClosed_integer {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] : IsClosed ↑v.integer

For any valuation v compatible with the valuative relation on R, the closed unit ball around zero {x | v x ≤ 1} is closed in the valuative topology.

theorem Valuation.isClopen_integer {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] : IsClopen ↑v.integer

For any valuation v compatible with the valuative relation on R, the closed unit ball around zero {x | v x ≤ 1} is clopen in the valuative topology.

theorem Valuation.isOpen_valuationSubring {K : Type u_2} [Field K] [ValuativeRel K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible] : IsOpen ↑v.valuationSubring

For any valuation v compatible with the valuative relation on a field K, the valuation subring defined by v is open in the valuative topology.

theorem Valuation.isClosed_valuationSubring {K : Type u_2} [Field K] [ValuativeRel K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible] : IsClosed ↑v.valuationSubring

For any valuation v compatible with the valuative relation on a field K, the valuation subring defined by v is closed in the valuative topology.

theorem Valuation.isClopen_valuationSubring {K : Type u_2} [Field K] [ValuativeRel K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible] : IsClopen ↑v.valuationSubring

For any valuation v compatible with the valuative relation on a field K, the valuation subring defined by v is clopen in the valuative topology.

@[deprecated Valuation.isOpen_ball (since := "2026-03-17")]

theorem IsValuativeTopology.isOpen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsOpen {x : R | v.restrict x < r}

Alias of Valuation.isOpen_ball.

---

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is open in the valuative topology.

@[deprecated Valuation.isClosed_ball (since := "2026-03-17")]

theorem IsValuativeTopology.isClosed_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClosed {x : R | v.restrict x < r}

Alias of Valuation.isClosed_ball.

---

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is closed in the valuative topology.

@[deprecated Valuation.isClopen_ball (since := "2026-03-17")]

theorem IsValuativeTopology.isClopen_ball {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClopen {x : R | v.restrict x < r}

Alias of Valuation.isClopen_ball.

---

For any valuation v compatible with the valuative relation on R, the open r-ball around zero {x | v.restrict x < r} is clopen in the valuative topology.

@[deprecated Valuation.isOpen_closedBall (since := "2026-03-17")]

theorem IsValuativeTopology.isOpen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsOpen {x : R | v.restrict x ≤ r}

Alias of Valuation.isOpen_closedBall.

---

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is open in the valuative topology.

@[deprecated Valuation.isClosed_closedBall (since := "2026-03-17")]

theorem IsValuativeTopology.isClosed_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] (r : MonoidWithZeroHom.ValueGroup₀ v) : IsClosed {x : R | v.restrict x ≤ r}

Alias of Valuation.isClosed_closedBall.

---

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is closed in the valuative topology.

@[deprecated Valuation.isClopen_closedBall (since := "2026-03-17")]

theorem IsValuativeTopology.isClopen_closedBall {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsClopen {x : R | v.restrict x ≤ r}

Alias of Valuation.isClopen_closedBall.

---

For any valuation v compatible with the valuative relation on R, the closed r-ball around zero {x | v.restrict x ≤ r} is clopen in the valuative topology.

@[deprecated Valuation.isClopen_sphere (since := "2026-03-17")]

theorem IsValuativeTopology.isClopen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsClopen {x : R | v.restrict x = r}

Alias of Valuation.isClopen_sphere.

---

For any valuation v compatible with the valuative relation on R, the sphere of radius r around zero {x | v.restrict x = r} is clopen in the valuative topology.

@[deprecated Valuation.isOpen_sphere (since := "2026-03-17")]

theorem IsValuativeTopology.isOpen_sphere {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible] {r : MonoidWithZeroHom.ValueGroup₀ v} (hr : r ≠ 0) : IsOpen {x : R | v.restrict x = r}

Alias of Valuation.isOpen_sphere.

---

For any valuation v compatible with the valuative relation on R, the sphere of radius r around zero {x | v.restrict x = r} is open in the valuative topology.