{R : Type u} →
  [inst : Ring R] →
    {Γ₀ : outParam (Type v)} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        (IsOpen : Set R → Prop) →
          (isOpen_univ : IsOpen Set.univ) →
            (isOpen_inter : ∀ (s t : Set R), IsOpen s → IsOpen t → IsOpen (s ∩ t)) →
              (isOpen_sUnion : ∀ (s : Set (Set R)), (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)) →
                (uniformity : Filter (R × R)) →
                  (symm : Filter.Tendsto Prod.swap uniformity uniformity) →
                    (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity) →
                      (nhds_eq_comap_uniformity : ∀ (x : R), nhds x = Filter.comap (Prod.mk x) uniformity) →
                        (UniformContinuous fun p => p.1 - p.2) →
                          (v : Valuation R Γ₀) → (∀ (s : Set R), s ∈ nhds 0 ↔ ∃ γ, {x | v x < ↑γ} ⊆ s) → Valued R Γ₀