comap_rename

Mathlib.Algebra.MvPolynomial.Comap

URI: https://scilib.ai/kg/mathlib#MvPolynomial.comap_rename

English

For any f : σ → τ and x : τ → R, comap (rename f) x equals x ∘ f.

Русский

Для отображения f: σ → τ и любого x: τ → R, comap (rename f) x = x ∘ f.

LaTeX

$$$\\operatorname{comap}(\\mathrm{rename}\\, f)\\, x = x \\circ f$$$

Lean4

theorem comap_rename (f : σ → τ) (x : τ → R) : comap (rename f) x = x ∘ f :=
  by
  funext
  simp [rename_X, comap_apply, aeval_X]

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

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

Разделы

Аффилиация

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