res — Mathlib

English

Turn a total function f into a partial function with domain s by restricting the lift of f to s.

Русский

Преобразовать полную функцию f в частичную с областью определения s путём ограничения Lift f до s.

LaTeX

$$$\\mathrm{res}(f,s) = (\\mathrm{PFun.lift}(f)).\\restrict\\; s.\\text{subset\_univ}$$$

Lean4

/-- Turns a function into a partial function with a prescribed domain. -/
def res (f : α → β) (s : Set α) : α →. β :=
  (PFun.lift f).restrict s.subset_univ

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