untiltFun — Mathlib

English

The untiltFun map assigns to each f ∈ PreTilt(O, p) an element of O, defined as the chosen limit from the exists_smodEq_untiltAux construction.

Русский

Функция untiltFun каждому f ∈ PreTilt(O, p) сопоставляет элемент O, заданный выбранной границей из построения exists_smodEq_untiltAux.

LaTeX

$$untiltFun: PreTilt(O,p) → O$$

Lean4

/-- Given a `p`-adically complete ring `O`, this is the underlying function of the untilt map.
It is defined as the limit of `p^n`-th powers of arbitrary lifts in `O` of the
`n`-th component from the perfection of `O/p`.
-/
def untiltFun (x : PreTilt O p) : O :=
  Classical.choose <| x.exists_smodEq_untiltAux

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