support_embDomain

Mathlib.Data.Finsupp.Defs

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

English

For injective e, the supports satisfy equality: supp(mapRange e f) = supp(f)

Русский

При инъективной e опоры удовлетворяют равенству: supp(mapRange e f) = supp(f).

LaTeX

$$support_mapRange_of_injective (e hf) (f) (he : Injective e) : supp(mapRange e hf f) = supp f$$

Lean4

@[simp]
theorem support_embDomain (f : α ↪ β) (v : α →₀ M) : (embDomain f v).support = v.support.map f :=
  rfl

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

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

Разделы

Аффилиация

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