of — Mathlib · SciLib

English

If s belongs to the support of v, then for any a we have v(a+s) = v(a).

Русский

Если s принадлежит опоре v, то для всякого a выполняется v(a+s) = v(a).

LaTeX

$$∀ a, ∀ s ∈ supp(v) : v(a+s) = v(a)$$

Lean4

/-- An alternate constructor of `AddValuation`, that doesn't reference `Multiplicative Γ₀ᵒᵈ` -/
def of : AddValuation R Γ₀ where
  toFun := f
  map_one' := h1
  map_zero' := h0
  map_add_le_max' := hadd
  map_mul' := hmul

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