English
If v IsEquiv v' and f is an injective, monotone, top-preserving map between value groups, then the mapped valuations are equivalent: (v.map f ht hf).IsEquiv (v'.map f ht hf).
Русский
Если v IsEquiv v' и f инъективен, монотонен и сохраняет топ, то отображённые оценки эквивалентны: (v.map f ht hf).IsEquiv (v'.map f ht hf).
LaTeX
$$$$ (v.map f ht hf).IsEquiv (v'.map f ht hf). $$$$
Lean4
theorem map {v' : AddValuation R Γ₀} (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone f) (inf : Injective f)
(h : v.IsEquiv v') : (v.map f ht hf).IsEquiv (v'.map f ht hf) :=
@Valuation.IsEquiv.map R (Multiplicative Γ₀ᵒᵈ) (Multiplicative Γ'₀ᵒᵈ) _ _ _ _ _
{ toFun := f
map_mul' := f.map_add
map_one' := f.map_zero
map_zero' := ht } (fun _x _y h => hf h) inf h
