map_apply

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#AddValuation.map_apply

English

For any f, ht, hf, v, and r ∈ R, applying v.map f ht hf to r yields f(v(r)).

Русский

Для любых f, ht, hf, v и r ∈ R применение v.map f ht hf к r даёт f(v(r)).

LaTeX

$$$$ (v.map f ht hf)(r) = f(v(r)). $$$$

Lean4

@[simp]
theorem map_apply (f : Γ₀ →+ Γ'₀) (ht : f ⊤ = ⊤) (hf : Monotone f) (v : AddValuation R Γ₀) (r : R) :
    v.map f ht hf r = f (v r) :=
  rfl

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

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

Разделы

Аффилиация

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