# 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 #

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
• = {a : α | (f a).Dom}
Instances For
@[simp]
theorem PFun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x ∃ (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 : α →. β) :
= {x : α | ∃ (y : β), y f x}
def PFun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
PFun.Dom f aβ

Evaluate a partial function

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

Evaluate a partial function to return an Option

Equations
Instances For
theorem PFun.ext' {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H1 : ∀ (a : α), a a ) (H2 : ∀ (a : α) (p : PFun.Dom f a) (q : PFun.Dom g a), PFun.fn f a p = PFun.fn g 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 : ()) :
β

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

Equations
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 ) :
PFun.asSubtype f { val := x, property := 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 : αβ) :
PFun.Dom f = 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
• = {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
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
• = {b : β | ∃ (a : α), b f a}
Instances For
def PFun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : Set α} (H : p ) :
α →. β

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 ) (a : α) (b : β) :
b 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 ∃ (y : β), (x, y)
theorem PFun.lift_graph {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
(a, b) 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
Instances For
@[simp]
theorem PFun.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : βα →. γ) (a : α) :
PFun.bind f g a = Part.bind (f a) 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
theorem PFun.bind_defined {α : Type u_7} {β : Type u_8} {γ : Type u_8} (p : Set α) {f : α →. β} {g : βα →. γ} (H1 : p ) (H2 : ∀ (x : β), p PFun.Dom (g x)) :
p PFun.Dom (f >>= g)
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 PFun.fix f a) :
(f a).Dom
theorem PFun.mem_fix_iff {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} :
b PFun.fix f a f a ∃ (a' : α), Sum.inr a' f a b PFun.fix f a'
theorem PFun.fix_stop {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {a : α} (hb : f 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) :

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 PFun.fix f a) (ha' : Sum.inr a' f a) :
b PFun.fix f a'
def PFun.fixInduction {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b PFun.fix f a) (H : (a' : α) → b PFun.fix f 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 PFun.fix f a) (H : (a' : α) → b PFun.fix f a'((a'' : α) → Sum.inr a'' f a'C a'')C a') :
= H a h fun (a' : α) (h' : Sum.inr a' f a) => PFun.fixInduction (_ : b PFun.fix f a') H
def PFun.fixInduction' {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b PFun.fix f a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b PFun.fix f 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 PFun.fix f a) (fa : f a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b PFun.fix f 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 PFun.fix f a) (h' : b PFun.fix f a') (fa : Sum.inr a' f a) (hbase : (a_final : α) → f a_finalC a_final) (hind : (a₀ a₁ : α) → b PFun.fix f 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
Instances For
theorem PFun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) :
= {y : β | ∃ x ∈ s, y f x}
theorem PFun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : Set α) :
y ∃ x ∈ s, y f x
theorem PFun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set α} {t : Set α} (h : s t) :
theorem PFun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
theorem PFun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
PFun.image f (s 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 β) :
= {x : α | ∃ y ∈ s, y f x}
@[simp]
theorem PFun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α) :
x ∃ y ∈ s, y f x
theorem PFun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
theorem PFun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
theorem PFun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
theorem PFun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
theorem PFun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
PFun.preimage f Set.univ =
theorem PFun.coe_preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
PFun.preimage (f) 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
Instances For
theorem PFun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
= {x : α | yf x, y s}
@[simp]
theorem PFun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : Set β) :
x yf x, y s
theorem PFun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
()
theorem PFun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
theorem PFun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
PFun.core f (s t) =
theorem PFun.mem_core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (x : α) :
x PFun.core (PFun.res f s) t x sf x t
theorem PFun.core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
theorem PFun.core_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
PFun.core (f) s = f ⁻¹' s
theorem PFun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
theorem PFun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
=
theorem PFun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
= ()
theorem PFun.preimage_asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
= Subtype.val ⁻¹'
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 : αβ) :
PFun.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
Instances For
@[simp]
theorem PFun.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : α) :
PFun.comp f g a = Part.bind (g a) f
@[simp]
theorem PFun.id_comp {α : Type u_1} {β : Type u_2} (f : α →. β) :
PFun.comp () f = f
@[simp]
theorem PFun.comp_id {α : Type u_1} {β : Type u_2} (f : α →. β) :
PFun.comp f () = f
@[simp]
theorem PFun.dom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
@[simp]
theorem PFun.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ) :
@[simp]
theorem PFun.Part.bind_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : Part α) :
@[simp]
theorem PFun.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ →. δ) (g : β →. γ) (h : α →. β) :
theorem PFun.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
(g f) = PFun.comp g f
def PFun.prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
α →. β × γ

Product of partial functions.

Equations
• = { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom)) }
Instances For
@[simp]
theorem PFun.dom_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
PFun.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 : ().Dom) :
().get h = ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom))
@[simp]
theorem PFun.prodLift_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) :
= { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom)) }
theorem PFun.mem_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
y 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
• PFun.prodMap f 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 (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom)) }
Instances For
@[simp]
theorem PFun.dom_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
PFun.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 : (PFun.prodMap f g x).Dom) :
(PFun.prodMap f g x).get h = ((f x.1).get (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom))
@[simp]
theorem PFun.prodMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) :
PFun.prodMap f 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 (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom)) }
theorem PFun.mem_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} :
y PFun.prodMap f 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 : β →. δ) :
PFun.prodLift (PFun.comp f Prod.fst) (PFun.comp g Prod.snd) =
@[simp]
theorem PFun.prodMap_id_id {α : Type u_1} {β : Type u_2} :
PFun.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₂ : ε →. ι) :
PFun.prodMap (PFun.comp f₂ f₁) (PFun.comp g₂ g₁) = PFun.comp (PFun.prodMap f₂ g₂) (PFun.prodMap f₁ g₁)