Check Equivalent relation

Stream: new members

[Wenrong Zou]

Hi everyone, I'm new in Lean.

import Mathlib.Topology.Algebra.ValuedField
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.Logic.Equiv.Defs
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Real.NNReal

structure ValuationEqui
    (v : Type _) (v' : Type _) {K : Type _} [Field K] {Γ : Type _}
    (v : Valuation K NNReal) (v' : Valuation K NNReal)
    where
      valequi : ∃ (s : ℝ), ∀ (x : K), 0 < s → (v x) = (v' x) ^ s

As you can see, I have define a new structure which is about the valuation of Field K. The thing I want to do is that I have (v1, v2, v3 : Valuation K NNReal) and v1, v2 is ValuationEqui and v2, v3 is ValuationEqui. I want to show that v1, v3 is ValuationEqui. In short, I want to show that ValuationEqui is an Equivalent relation. How could I achieve this.
Thanks in advance.

[Mario Carneiro]

the logical form of valequi looks suspicious: it is satisfied for any valuation by setting s = 0

[Wenrong Zou]

Mario Carneiro 发言道：

the logical form of valequi looks suspicious: it is satisfied for any valuation by setting s = 0

I have assume that s should be positive.

[Mario Carneiro]

you said that if s is positive then some property follows. If s is not positive then it is trivially satisfied

[Wenrong Zou]

Mario Carneiro 发言道：

you said that if s is positive then some property follows. If s is not positive then it is trivially satisfied

Oh, I made a grammar mistake. Thank you very much.