Theorems · Definition · order theory

Set.domRestrict

{α : Type u_1} → {π : α → Type u_6} → (s : Set α) → ((a : α) → π a) → (a : ↑s) → π ↑a

Restrict domain of a function f to a set s. Same as Subtype.restrict but this version takes an argument ↥s instead of Subtype s.

Defined in

Mathlib.Data.Set.Restrict

Cited by

383 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 10 definitions · uses no axioms