comapDomain_mapDomain

Mathlib.Data.Finsupp.Basic

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

← MathLib Explorer

English

For any injective f, comapDomain f (mapDomain f l) hf = l.

Русский

Для любого инъективного f, comapDomain f (mapDomain f l) hf = l.

LaTeX

$$$$ \mathrm{comapDomain}\ f\ (\mathrm{mapDomain}\ f\ l) hf.injOn = l. $$$$

Lean4

theorem comapDomain_mapDomain (hf : Function.Injective f) (l : α →₀ M) : comapDomain f (mapDomain f l) hf.injOn = l :=
  by ext; rw [comapDomain_apply, mapDomain_apply hf]

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

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

Разделы

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

Аффилиация

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