# Partial functions #

This file defines partial functions. Partial functions are like functions, except they can also be "undefined" on some inputs. We define them as functions α → Part β.

## Definitions #

• PFun α β: Type of partial functions from α to β. Defined as α → Part β and denoted α →. β.
• PFun.Dom: Domain of a partial function. Set of values on which it is defined. Not to be confused with the domain of a function α → β, which is a type (α presently).
• PFun.fn: Evaluation of a partial function. Takes in an element and a proof it belongs to the partial function's Dom.
• PFun.asSubtype: Returns a partial function as a function from its Dom.
• PFun.toSubtype: Restricts the codomain of a function to a subtype.
• PFun.evalOpt: Returns a partial function with a decidable Dom as a function a → Option β.
• PFun.lift: Turns a function into a partial function.
• PFun.id: The identity as a partial function.
• PFun.comp: Composition of partial functions.
• PFun.restrict: Restriction of a partial function to a smaller Dom.
• PFun.res: Turns a function into a partial function with a prescribed domain.
• PFun.fix : First return map of a partial function f : α →. β ⊕ α.
• PFun.fix_induction: A recursion principle for PFun.fix.

### Partial functions as relations #

Partial functions can be considered as relations, so we specialize some Rel definitions to PFun:

• PFun.image: Image of a set under a partial function.
• PFun.ran: Range of a partial function.
• PFun.preimage: Preimage of a set under a partial function.
• PFun.core: Core of a set under a partial function.
• PFun.graph: Graph of a partial function a →. βas a Set (α × β).
• PFun.graph': Graph of a partial function a →. βas a Rel α β.

### PFun α as a monad #

• PFun.pure: The monad pure function, the constant x function.
• PFun.bind: The monad bind function, pointwise Part.bind
• PFun.map: The monad map function, pointwise Part.map.
def PFun (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

PFun α β, or α →. β, is the type of partial functions from α to β. It is defined as α → Part β.

Equations
Instances For

α →. β is notation for the type PFun α β of partial functions from α to β.

Equations
Instances For
instance PFun.inhabited {α : Type u_1} {β : Type u_2} :
Inhabited (α →. β)
Equations
• PFun.inhabited = { default := fun (x : α) => Part.none }
def PFun.Dom {α : Type u_1} {β : Type u_2} (f : α →. β) :
Set α

The domain of a partial function

Equations
• f.Dom = {a : α | (f a).Dom}
Instances For
@[simp]
theorem PFun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x f.Dom ∃ (y : β), y f x
@[simp]
theorem PFun.dom_mk {α : Type u_1} {β : Type u_2} (p : αProp) (f : (a : α) → p aβ) :
(PFun.Dom fun (x : α) => { Dom := p x, get := f x }) = {x : α | p x}
theorem PFun.dom_eq {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.Dom = {x : α | ∃ (y : β), y f x}
def PFun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
f.Dom aβ

Evaluate a partial function

Equations
• f.fn a = (f a).get
Instances For
@[simp]
theorem PFun.fn_apply {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
f.fn a = (f a).get
def PFun.evalOpt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : DecidablePred fun (x : α) => x f.Dom] (x : α) :

Evaluate a partial function to return an Option

Equations
• f.evalOpt x = (f x).toOption
Instances For
theorem PFun.ext' {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H1 : ∀ (a : α), a f.Dom a g.Dom) (H2 : ∀ (a : α) (p : f.Dom a) (q : g.Dom a), f.fn a p = g.fn a q) :
f = g

Partial function extensionality

theorem PFun.ext {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H : ∀ (a : α) (b : β), b f a b g a) :
f = g
def PFun.asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : f.Dom) :
β

Turns a partial function into a function out of its domain.

Equations
• f.asSubtype s = f.fn s
Instances For
def PFun.equivSubtype {α : Type u_1} {β : Type u_2} :
(α →. β) (p : αProp) × (β)

The type of partial functions α →. β is equivalent to the type of pairs (p : α → Prop, f : Subtype p → β).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PFun.asSubtype_eq_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β} (fxy : y f x) (domx : x f.Dom) :
f.asSubtype x, domx = y
def PFun.lift {α : Type u_1} {β : Type u_2} (f : αβ) :
α →. β

Turn a total function into a partial function.

Equations
Instances For
instance PFun.coe {α : Type u_1} {β : Type u_2} :
Coe (αβ) (α →. β)
Equations
• PFun.coe = { coe := PFun.lift }
@[simp]
theorem PFun.coe_val {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
f a = Part.some (f a)
@[simp]
theorem PFun.dom_coe {α : Type u_1} {β : Type u_2} (f : αβ) :
(f).Dom = Set.univ
theorem PFun.lift_injective {α : Type u_1} {β : Type u_2} :
def PFun.graph {α : Type u_1} {β : Type u_2} (f : α →. β) :
Set (α × β)

Graph of a partial function f as the set of pairs (x, f x) where x is in the domain of f.

Equations
• f.graph = {p : α × β | p.2 f p.1}
Instances For
def PFun.graph' {α : Type u_1} {β : Type u_2} (f : α →. β) :
Rel α β

Graph of a partial function as a relation. x and y are related iff f x is defined and "equals" y.

Equations
• f.graph' x y = (y f x)
Instances For
def PFun.ran {α : Type u_1} {β : Type u_2} (f : α →. β) :
Set β

The range of a partial function is the set of values f x where x is in the domain of f.

Equations
• f.ran = {b : β | ∃ (a : α), b f a}
Instances For
def PFun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : Set α} (H : p f.Dom) :
α →. β

Restrict a partial function to a smaller domain.

Equations
Instances For
@[simp]
theorem PFun.mem_restrict {α : Type u_1} {β : Type u_2} {f : α →. β} {s : Set α} (h : s f.Dom) (a : α) (b : β) :
b f.restrict h a a s b f a
def PFun.res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
α →. β

Turns a function into a partial function with a prescribed domain.

Equations
Instances For
theorem PFun.mem_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (a : α) (b : β) :
b PFun.res f s a a s f a = b
theorem PFun.res_univ {α : Type u_1} {β : Type u_2} (f : αβ) :
PFun.res f Set.univ = f
theorem PFun.dom_iff_graph {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x f.Dom ∃ (y : β), (x, y) f.graph
theorem PFun.lift_graph {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
(a, b) (f).graph f a = b
def PFun.pure {α : Type u_1} {β : Type u_2} (x : β) :
α →. β

The monad pure function, the total constant x function

Equations
Instances For
def PFun.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : βα →. γ) :
α →. γ

The monad bind function, pointwise Part.bind

Equations
• f.bind g a = (f a).bind fun (b : β) => g b a
Instances For
@[simp]
theorem PFun.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : βα →. γ) (a : α) :
f.bind g a = (f a).bind fun (b : β) => g b a
def PFun.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (g : α →. β) :
α →. γ

The monad map function, pointwise Part.map

Equations
Instances For
instance PFun.monad {α : Type u_1} :
Equations
instance PFun.lawfulMonad {α : Type u_1} :
Equations
• =
theorem PFun.pure_defined {α : Type u_1} {β : Type u_2} (p : Set α) (x : β) :
p ().Dom
theorem PFun.bind_defined {α : Type u_7} {β : Type u_8} {γ : Type u_8} (p : Set α) {f : α →. β} {g : βα →. γ} (H1 : p f.Dom) (H2 : ∀ (x : β), p (g x).Dom) :
p (f >>= g).Dom
def PFun.fix {α : Type u_1} {β : Type u_2} (f : α →. β α) :
α →. β

First return map. Transforms a partial function f : α →. β ⊕ α into the partial function α →. β which sends a : α to the first value in β it hits by iterating f, if such a value exists. By abusing notation to illustrate, either f a is in the β part of β ⊕ α (in which case f.fix a returns f a), or it is undefined (in which case f.fix a is undefined as well), or it is in the α part of β ⊕ α (in which case we repeat the procedure, so f.fix a will return f.fix (f a)).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PFun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} (h : b f.fix a) :
(f a).Dom
theorem PFun.mem_fix_iff {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} :
b f.fix a f a ∃ (a' : α), Sum.inr a' f a b f.fix a'
theorem PFun.fix_stop {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {a : α} (hb : f a) :
b f.fix a

If advancing one step from a leads to b : β, then f.fix a = b

theorem PFun.fix_fwd_eq {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {a' : α} (ha' : Sum.inr a' f a) :
f.fix a = f.fix a'

If advancing one step from a on f leads to a' : α, then f.fix a = f.fix a'

theorem PFun.fix_fwd {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {a : α} {a' : α} (hb : b f.fix a) (ha' : Sum.inr a' f a) :
b f.fix a'
def PFun.fixInduction {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (H : (a' : α) → b f.fix a'((a'' : α) → Sum.inr a'' f a'C a'')C a') :
C a

A recursion principle for PFun.fix.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PFun.fixInduction_spec {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (H : (a' : α) → b f.fix a'((a'' : α) → Sum.inr a'' f a'C a'')C a') :
= H a h fun (a' : α) (h' : Sum.inr a' f a) =>
def PFun.fixInduction' {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
C a

Another induction lemma for b ∈ f.fix a which allows one to prove a predicate P holds for a given that f a inherits P from a and P holds for preimages of b.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem PFun.fixInduction'_stop {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (fa : f a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
PFun.fixInduction' h hbase hind = hbase a fa
theorem PFun.fixInduction'_fwd {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} {a' : α} (h : b f.fix a) (h' : b f.fix a') (fa : Sum.inr a' f a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
PFun.fixInduction' h hbase hind = hind a a' h' fa (PFun.fixInduction' h' hbase hind)
def PFun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) :
Set β

Image of a set under a partial function.

Equations
• f.image s = f.graph'.image s
Instances For
theorem PFun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) :
f.image s = {y : β | xs, y f x}
theorem PFun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : Set α) :
y f.image s xs, y f x
theorem PFun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set α} {t : Set α} (h : s t) :
f.image s f.image t
theorem PFun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
f.image (s t) f.image s f.image t
theorem PFun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
f.image (s t) = f.image s f.image t
def PFun.preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
Set α

Preimage of a set under a partial function.

Equations
Instances For
theorem PFun.Preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.preimage s = {x : α | ys, y f x}
@[simp]
theorem PFun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α) :
x f.preimage s ys, y f x
theorem PFun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.preimage s f.Dom
theorem PFun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
f.preimage s f.preimage t
theorem PFun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
f.preimage (s t) f.preimage s f.preimage t
theorem PFun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
f.preimage (s t) = f.preimage s f.preimage t
theorem PFun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.preimage Set.univ = f.Dom
theorem PFun.coe_preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
(f).preimage s = f ⁻¹' s
def PFun.core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : 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.

Equations
• f.core s = f.graph'.core s
Instances For
theorem PFun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.core s = {x : α | yf x, y s}
@[simp]
theorem PFun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : Set β) :
x f.core s yf x, y s
theorem PFun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.Dom f.core s
theorem PFun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
f.core s f.core t
theorem PFun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
f.core (s t) = f.core s f.core t
theorem PFun.mem_core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (x : α) :
x (PFun.res f s).core t x sf x t
theorem PFun.core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
(PFun.res f s).core t = s f ⁻¹' t
theorem PFun.core_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
(f).core s = f ⁻¹' s
theorem PFun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.preimage s f.core s
theorem PFun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.preimage s = f.core s f.Dom
theorem PFun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.core s = f.preimage s f.Dom
theorem PFun.preimage_asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s
def PFun.toSubtype {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) :
α →.

Turns a function into a partial function to a subtype.

Equations
Instances For
@[simp]
theorem PFun.dom_toSubtype {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) :
().Dom = {a : α | p (f a)}
@[simp]
theorem PFun.toSubtype_apply {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) (a : α) :
= { Dom := p (f a), get := Subtype.mk (f a) }
theorem PFun.dom_toSubtype_apply_iff {α : Type u_1} {β : Type u_2} {p : βProp} {f : αβ} {a : α} :
().Dom p (f a)
theorem PFun.mem_toSubtype_iff {α : Type u_1} {β : Type u_2} {p : βProp} {f : αβ} {a : α} {b : } :
b b = f a
def PFun.id (α : Type u_7) :
α →. α

The identity as a partial function

Equations
• = Part.some
Instances For
@[simp]
theorem PFun.coe_id (α : Type u_7) :
id =
@[simp]
theorem PFun.id_apply {α : Type u_1} (a : α) :
PFun.id α a =
def PFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
α →. γ

Composition of partial functions as a partial function.

Equations
• f.comp g a = (g a).bind f
Instances For
@[simp]
theorem PFun.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : α) :
f.comp g a = (g a).bind f
@[simp]
theorem PFun.id_comp {α : Type u_1} {β : Type u_2} (f : α →. β) :
().comp f = f
@[simp]
theorem PFun.comp_id {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.comp () = f
@[simp]
theorem PFun.dom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
(f.comp g).Dom = g.preimage f.Dom
@[simp]
theorem PFun.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ) :
(f.comp g).preimage s = g.preimage (f.preimage s)
@[simp]
theorem PFun.Part.bind_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : Part α) :
a.bind (f.comp g) = (a.bind g).bind f
@[simp]
theorem PFun.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ →. δ) (g : β →. γ) (h : α →. β) :
(f.comp g).comp h = f.comp (g.comp h)
theorem PFun.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
(g f) = (g).comp f
def PFun.prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
α →. β × γ

Product of partial functions.

Equations
• f.prodLift g x = { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get , (g x).get ) }
Instances For
@[simp]
theorem PFun.dom_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
(f.prodLift g).Dom = {x : α | (f x).Dom (g x).Dom}
theorem PFun.get_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) (h : (f.prodLift g x).Dom) :
(f.prodLift g x).get h = ((f x).get , (g x).get )
@[simp]
theorem PFun.prodLift_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) :
f.prodLift g x = { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get , (g x).get ) }
theorem PFun.mem_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
y f.prodLift g x y.1 f x y.2 g x
def PFun.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
α × β →. γ × δ

Product of partial functions.

Equations
• f.prodMap g x = { Dom := (f x.1).Dom (g x.2).Dom, get := fun (h : (f x.1).Dom (g x.2).Dom) => ((f x.1).get , (g x.2).get ) }
Instances For
@[simp]
theorem PFun.dom_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
(f.prodMap g).Dom = {x : α × β | (f x.1).Dom (g x.2).Dom}
theorem PFun.get_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) (h : (f.prodMap g x).Dom) :
(f.prodMap g x).get h = ((f x.1).get , (g x.2).get )
@[simp]
theorem PFun.prodMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) :
f.prodMap g x = { Dom := (f x.1).Dom (g x.2).Dom, get := fun (h : (f x.1).Dom (g x.2).Dom) => ((f x.1).get , (g x.2).get ) }
theorem PFun.mem_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} :
y f.prodMap g x y.1 f x.1 y.2 g x.2
@[simp]
theorem PFun.prodLift_fst_comp_snd_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
(f.comp Prod.fst).prodLift (g.comp Prod.snd) = f.prodMap g
@[simp]
theorem PFun.prodMap_id_id {α : Type u_1} {β : Type u_2} :
().prodMap () = PFun.id (α × β)
@[simp]
theorem PFun.prodMap_comp_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ι : Type u_6} (f₁ : α →. β) (f₂ : β →. γ) (g₁ : δ →. ε) (g₂ : ε →. ι) :
(f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)