restrict — Mathlib

English

Restriction operator is the map sending a function to its restriction on s, i.e., restricting the domain to s.

Русский

Оператор ограничения переводит функцию к её ограничению на множество s, то есть ограничение области определения до s.

LaTeX

$$$s\restrict (\pi := \pi) = \lambda f x. f x$$$

Lean4

/-- Restrict domain of a function `f` to a set `s`. Same as `Subtype.restrict` but this version
takes an argument `↥s` instead of `Subtype s`. -/
def restrict (s : Set α) (f : ∀ a : α, π a) : ∀ a : s, π a := fun x => f x

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