restrict_empty

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.restrict_empty

English

Restricting to the whole space leaves the function unchanged: restrict f univ = f.

Русский

Ограничение на всю вселенную оставляет функцию без изменений: restrict f univ = f.

LaTeX

$$$\\restrict f\\,\\mathrm{univ} = f.$$$

Lean4

@[simp]
theorem restrict_empty (f : α →ₛ β) : restrict f ∅ = 0 := by simp [restrict]

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

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

Разделы

Аффилиация

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