Theorems · Theorem · commutative algebra

Valuation.exists_setOf_restrict_le_iff

Deprecated since 2026-07-09Use Valuation.exists_setOfPred_restrict_le_iff instead.

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] (x : R) (s : Set R),
  (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation R) (a - x) < ↑γ} ⊆ s

Alias of Valuation.exists_setOfPred_restrict_le_iff.

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingValuativeRelLinearOrderedCommGroupWithZeroValuation.Compatible