ofAddValuation_apply — Mathlib

English

The value given by the inverse map from an AddValuation equals the original r-value mapped through the corresponding structure.

Русский

Значение, полученное обратным отображением от AddValuation, равно исходному значению r, преобразованному соответствующей структурой.

LaTeX

$$$ (ofAddValuation v)(r) = \\mathrm{Additive}.toMul( \\mathrm{OrderDual}.ofDual( v(r) ) ). $$$

Lean4

@[simp]
theorem ofAddValuation_apply (v : AddValuation R (Additive Γ₀)ᵒᵈ) (r : R) :
    ofAddValuation v r = Additive.toMul (OrderDual.ofDual (v r)) :=
  rfl

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