instCoeTCValuationOfValuationClass

English

There is a canonical coercion from any function f that is a valuation into a Valuation R Γ₀, respecting the valuation axioms (map_mul, map_one, map_zero, map_add_le_max).

Русский

Существует каноническое преобразование из любой функции f, являющейся оценкой, в Valuation R Γ₀, сохраняющее аксиомы оценки (умножение, единицу, ноль, ассоциативное свойство сложения через max).

LaTeX

$$$[\\text{FunLike } F R \\Gamma_0] \\;[\\text{ValuationClass } F R \\Gamma_0] \\Rightarrow \\mathrm{CoeTC}\; F (\\mathrm{Valuation } R \\Gamma_0).$$$

Lean4

instance [FunLike F R Γ₀] [ValuationClass F R Γ₀] : CoeTC F (Valuation R Γ₀) :=
  ⟨fun f =>
    { toFun := f
      map_one' := map_one f
      map_zero' := map_zero f
      map_mul' := map_mul f
      map_add_le_max' := map_add_le_max f }⟩

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