Theorems · Theorem · commutative algebra

IsValuativeTopology.isOpen_closedBall

Deprecated since 2026-03-17Use Valuation.isOpen_closedBall instead.

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsOpen {x | 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.

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroTopologicalSpaceIsValuativeTopologyValuation.Compatible