apply_equiv

Mathlib.Topology.Algebra.Valued.WithVal

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

English

For r in WithVal v, applying the equivalence and then evaluating with v gives the same as evaluating in WithVal’s valuation.

Русский

Для r из WithVal v применение эквивалента и затем оценка равны оценке в WithVal.

LaTeX

$$v (equiv v r) = Valued.v r$$

Lean4

theorem apply_equiv (r : WithVal v) : v (equiv v r) = Valued.v r :=
  rfl

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

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

Разделы

Аффилиация

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