restrict — Mathlib

English

Restrict a family of types to a finite subdomain: the restricted function on s maps i ∈ s to f(i).

Русский

Ограничение семейства типов до конечной подчасти: ограниченная функция на s отправляет i ∈ s в f(i).

LaTeX

$$$ \\text{restrict}(s, f) : (i ∈ s) \\to \\pi i := \\lambda i. f(i). $$$

Lean4

/-- Restrict domain of a function `f` to a finite set `s`. -/
@[simp]
def restrict (s : Finset ι) (f : (i : ι) → π i) : (i : s) → π i := fun x ↦ f x

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