mapDomain_equiv_apply

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.mapDomain_equiv_apply

← MathLib Explorer

English

For a bijection f, (mapDomain f x)(a) = x(f^{-1}(a)).

Русский

Для биекции f: (mapDomain f x)(a) = x(f^{-1}(a)).

LaTeX

$$$\\operatorname{mapDomain} f\\, x\\, a = x\\, (f^{-\\1}(a))$$$

Lean4

@[simp]
theorem mapDomain_equiv_apply {f : α ≃ β} (x : α →₀ M) (a : β) : mapDomain f x a = x (f.symm a) :=
  by
  conv_lhs => rw [← f.apply_symm_apply a]
  exact mapDomain_apply f.injective _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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