restrict_eqOn

Mathlib.Topology.LocallyFinsupp

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

← MathLib Explorer

English

On the domain V, the restricted function equals the original function; i.e., D.restrict h agrees with D on V.

Русский

На области V ограниченная функция совпадает с исходной на V.

LaTeX

$$$\\text{EqOn}((D.restrict h), D, V)$$$

Lean4

theorem restrict_eqOn [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : Set.EqOn (D.restrict h) D V :=
  by
  intro _ _
  simp_all [restrict_apply]

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

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

Разделы

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

Аффилиация

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