restrict — Mathlib

English

Restrict a partial function to a smaller domain p by ensuring p ⊆ f.Dom; the restricted function is defined on p by f(x) with the appropriate witness.

Русский

Ограничиваем частичную функцию до меньшей области p при условии p ⊆ Dom f; ограниченная функция определяется на p через f(x) с подходящим доказательством.

LaTeX

$$$f|_p = \\lambda x. (f(x)).\\restrict(x \\in p) (H x)$$$

Lean4

/-- Restrict a partial function to a smaller domain. -/
def restrict (f : α →. β) {p : Set α} (H : p ⊆ f.Dom) : α →. β := fun x => (f x).restrict (x ∈ p) (@H x)

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