some_embDomain_some

Mathlib.Data.Finsupp.Option

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

English

The embedding of the domain via some is an identity when composed with some: (f.embDomain .some).some = f.

Русский

Встраивание области через some восстанавливает исходную финспп: (f.embDomain .some).some = f.

LaTeX

$$$ (f.embDomain .some).some = f $$$

Lean4

@[simp]
theorem some_embDomain_some [Zero M] (f : α →₀ M) : (f.embDomain .some).some = f := by ext; rw [some_apply];
  exact embDomain_apply _ _ _

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

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

Разделы

Аффилиация

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