asFun — Mathlib

English

There is a canonical function extraction from an AddValuation to R → Γ0, denoted as asFun (deprecated in favor of the coercion), with asFun = v.

Русский

Существует каноническое отображение из AddValuation в R → Γ0, обозначаемое asFun (устаревшее, предпочтительнее ковариантная операция), с asFun = v.

LaTeX

$$$$ \mathrm{asFun} : R \rightarrow \Gamma_0 \quad\text{defined by } \mathrm{asFun} = v. $$$$

Lean4

/-- A helper function for Lean to inferring types correctly.

Deprecated since it is unused.
-/
@[deprecated "Use `⇑v` instead" (since := "2025-09-04")]
def asFun : R → Γ₀ :=
  v

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