restrict — Mathlib

English

The restriction of a continuous map f: α → β to a subset s ⊆ α is the map f|s : s → β given by f|s(x) = f(x).

Русский

Ограничение непрерывного отображения f: α → β на подмножество s ⊆ α задаёт отображение f|s: s → β, x ↦ f(x).

LaTeX

$$$\mathrm{restrict}(f) : C(s, \beta)\quad\text{with }\text{toFun}=f\circ((\uparrow):s\to\alpha)$$$

Lean4

/-- The restriction of a continuous function `α → β` to a subset `s` of `α`. -/
def restrict (f : C(α, β)) : C(s, β) where toFun := f ∘ ((↑) : s → α)

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