valuation

Mathlib.Topology.Algebra.Valued.WithVal

URI: https://scilib.ai/kg/mathlib#WithVal.valuation

English

There is a canonical valuation on the type WithVal v, transported from v along the canonical equivalence.

Русский

Существует каноническая оценка на тип WithVal v, перенесенная по каноническому эквиваленту от v.

LaTeX

$$valuation v = v ∘ (equiv v)$$

Lean4

/-- Canonical valuation on the `WithVal v` type synonym. -/
def valuation : Valuation (WithVal v) Γ₀ :=
  v.comap (equiv v)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru