Theorems · Definition · logic and foundations

PFun.core

{α : Type u_1} → {β : Type u_2} → (α →. β) → Set β → Set α

Core of a set s : Set β with respect to a partial function f : α →. β. Set of all a : α such that f a ∈ s, if f a is defined.

Defined in

Mathlib.Data.PFun

Cited by

16 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms