Theorems · Theorem · commutative algebra

IsValuativeTopology.hasBasis_nhds

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  (x : R), (nhds x).HasBasis (fun x => True) fun γ => {z | (ValuativeRel.valuation R) (z - x) < ↑γ}

Defined in

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingValuativeRelTopologicalSpaceIsValuativeTopology