comapDomain'_zero

Mathlib.Data.DFinsupp.Defs

URI: https://scilib.ai/kg/mathlib#DFinsupp.comapDomain'_zero

← MathLib Explorer

English

For the primed version, comapDomain' h hh' maps 0 to 0.

Русский

Для версии с апострофом, comapDomain' h hh' отображает 0 в 0.

LaTeX

$$$\\mathrm{comapDomain'}(h,hh')(0) = 0$$$

Lean4

@[simp]
theorem comapDomain'_zero [∀ i, Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) :
    comapDomain' h hh' (0 : Π₀ i, β i) = 0 := by
  ext
  rw [zero_apply, comapDomain'_apply, zero_apply]

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

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

Разделы

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

Аффилиация

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