isEquiv_of_map_strictMono — Mathlib

English

If f is a strictly monotone map between value groups, then mapping a valuation v by f yields an equivalent valuation to v.

Русский

Если отображение f между группами значений строго монотонно, то отображение валидации v через f сохраняет эквивалентность.

LaTeX

$$$ (\text{StrictMono } f) \rightarrow (v.map f) \IsEquiv v $$$

Lean4

theorem isEquiv_of_map_strictMono [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀] [Ring R]
    {v : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀) (H : StrictMono f) : IsEquiv (v.map f H.monotone) v := fun _x _y =>
  ⟨H.le_iff_le.mp, fun h => H.monotone h⟩

Похожие утверждения