restrict — Mathlib

English

Restriction of a map f to s with codomain t is the induced map s → t defined by x ↦ f(x).

Русский

Ограничение отображения f на s с кодом t задаёт взаимно определённое отображение s → t, которое отправляет x ↦ f(x).

LaTeX

$$$$\\text{restrict}(f, s, t, h) = \\text{Subtype.map}(f,h).$$$$

Lean4

/-- Given a map `f` sending `s : Set α` into `t : Set β`, restrict domain of `f` to `s`
and the codomain to `t`. Same as `Subtype.map`. -/
def restrict (f : α → β) (s : Set α) (t : Set β) (h : MapsTo f s t) : s → t :=
  Subtype.map f h

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