restrictMonoidHom_apply

Mathlib.Topology.LocallyFinsupp

URI: https://scilib.ai/kg/mathlib#Function.locallyFinsuppWithin.restrictMonoidHom_apply

← MathLib Explorer

English

The underlying function of restrictMonoidHom equals D.restrict h for a given D.

Русский

Умная функция restrictMonoidHom совпадает с D.restrict h на конкретном D.

LaTeX

$$$\\text{restrictMonoidHom}_h(D) = D.restrict h$$$

Lean4

@[simp]
theorem restrictMonoidHom_apply [AddCommGroup Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) :
    restrictMonoidHom h D = D.restrict h := by rfl

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

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

Разделы

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

Аффилиация

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