data.pfun

# Partial functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.as_subtype: Returns a partial function as a function from its dom.
• pfun.to_subtype: Restricts the codomain of a function to a subtype.
• pfun.eval_opt: 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 pfun
@[protected, instance]
def pfun.inhabited {α : Type u_1} {β : Type u_2} :
inhabited →. β)
Equations
def pfun.dom {α : Type u_1} {β : Type u_2} (f : α →. β) :
set α

The domain of a partial function

Equations
@[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 (λ (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
@[simp]
theorem pfun.fn_apply {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
f.fn a = (f a).get
def pfun.eval_opt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : decidable_pred (λ (_x : α), _x f.dom)] (x : α) :

Evaluate a partial function to return an option

Equations
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.as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : (f.dom)) :
β

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

Equations
def pfun.equiv_subtype {α : 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
theorem pfun.as_subtype_eq_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β} (fxy : y f x) (domx : x f.dom) :
f.as_subtype x, domx⟩ = y
@[protected]
def pfun.lift {α : Type u_1} {β : Type u_2} (f : α β) :
α →. β

Turn a total function into a partial function.

Equations
@[protected, instance]
def pfun.has_coe {α : Type u_1} {β : Type u_2} :
has_coe β) →. β)
Equations
@[simp]
theorem pfun.lift_eq_coe {α : Type u_1} {β : Type u_2} (f : α β) :
= f
@[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 : α β) :
theorem pfun.coe_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
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
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
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
@[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
theorem pfun.mem_res {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) (a : α) (b : β) :
b s a a s f a = b
theorem pfun.res_univ {α : Type u_1} {β : Type u_2} (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
@[protected]
def pfun.pure {α : Type u_1} {β : Type u_2} (x : β) :
α →. β

The monad pure function, the total constant x function

Equations
• = λ (_x : α),
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 (λ (b : β), g b a)
@[simp]
theorem pfun.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : β α →. γ) (a : α) :
f.bind g a = (f a).bind (λ (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
• g = λ (a : α), (g a)
@[protected, instance]
def pfun.monad {α : Type u_1} :
Equations
@[protected, instance]
def pfun.is_lawful_monad {α : Type u_1} :
theorem pfun.pure_defined {α : Type u_1} {β : Type u_2} (p : set α) (x : β) :
theorem pfun.bind_defined {α : Type u_1} {β γ : Type u_2} (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
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.fix_induction {α : Type u_1} {β : Type u_2} {C : α Sort u_3} {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
theorem pfun.fix_induction_spec {α : Type u_1} {β : Type u_2} {C : α Sort u_3} {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 (λ (a' : α) (h' : sum.inr a' f a),
def pfun.fix_induction' {α : Type u_1} {β : Type u_2} {C : α Sort u_3} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (hbase : Π (a_final : α), f a_final C 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
• hbase hind = (λ (a' : α) (h : b f.fix a') (ih : Π (a'' : α), sum.inr a'' f a' C a''), (λ (_x : β α) (e : (f a').get _ = _x), _x.cases_on (λ (b' : β) (e : (f a').get _ = sum.inl b'), hbase a' _) (λ (a'' : α) (e : (f a').get _ = sum.inr a''), hind a' a'' _ _ (ih a'' _)) e) ((f a').get _) _)
theorem pfun.fix_induction'_stop {α : Type u_1} {β : Type u_2} {C : α Sort u_3} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (fa : f a) (hbase : Π (a_final : α), f a_final C a_final) (hind : Π (a₀ a₁ : α), b f.fix a₁ sum.inr a₁ f a₀ C a₁ C a₀) :
hbase hind = hbase a fa
theorem pfun.fix_induction'_fwd {α : Type u_1} {β : Type u_2} {C : α Sort u_3} {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_final C a_final) (hind : Π (a₀ a₁ : α), b f.fix a₁ sum.inr a₁ f a₀ C a₁ C a₀) :
hbase hind = hind a a' h' fa hbase hind)
def pfun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
set β

Image of a set under a partial function.

Equations
theorem pfun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
f.image s = {y : β | (x : α) (H : x s), y f x}
theorem pfun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : set α) :
y f.image s (x : α) (H : x s), y f x
theorem pfun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set α} (h : s t) :
f.image s f.image t
theorem pfun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set α) :
f.image (s t) f.image s f.image t
theorem pfun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s 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
theorem pfun.preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s = {x : α | (y : β) (H : y s), y f x}
@[simp]
theorem pfun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) (x : α) :
x f.preimage s (y : β) (H : 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 t : set β} (h : s t) :
theorem pfun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
theorem pfun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.preimage (s t) = f.preimage s f.preimage t
theorem pfun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
= f.dom
theorem pfun.coe_preimage {α : Type u_1} {β : Type u_2} (f : α β) (s : set β) :
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
theorem pfun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.core s = {x : α | (y : β), y f x y s}
@[simp]
theorem pfun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : set β) :
x f.core s (y : β), y f 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 t : set β} (h : s t) :
f.core s f.core t
theorem pfun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s 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 s f 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 β) :
theorem pfun.preimage_as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
=
def pfun.to_subtype {α : Type u_1} {β : Type u_2} (p : β Prop) (f : α β) :
α →.

Turns a function into a partial function to a subtype.

Equations
@[simp]
theorem pfun.dom_to_subtype {α : Type u_1} {β : Type u_2} (p : β Prop) (f : α β) :
f).dom = {a : α | p (f a)}
@[simp]
theorem pfun.to_subtype_apply {α : Type u_1} {β : Type u_2} (p : β Prop) (f : α β) (a : α) :
a = {dom := p (f a), get := subtype.mk (f a)}
theorem pfun.dom_to_subtype_apply_iff {α : Type u_1} {β : Type u_2} {p : β Prop} {f : α β} {a : α} :
f a).dom p (f a)
theorem pfun.mem_to_subtype_iff {α : Type u_1} {β : Type u_2} {p : β Prop} {f : α β} {a : α} {b : subtype p} :
b a b = f a
@[protected]
def pfun.id (α : Type u_1) :
α →. α

The identity as a partial function

Equations
@[simp]
theorem pfun.coe_id (α : Type u_1) :
@[simp]
theorem pfun.id_apply {α : Type u_1} (a : α) :
a =
def pfun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
α →. γ

Composition of partial functions as a partial function.

Equations
@[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 : α →. β) :
(pfun.id β).comp f = f
@[simp]
theorem pfun.comp_id {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.comp (pfun.id α) = 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 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.prod_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
α →. β × γ

Product of partial functions.

Equations
@[simp]
theorem pfun.dom_prod_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
(f.prod_lift g).dom = {x : α | (f x).dom (g x).dom}
theorem pfun.get_prod_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) (h : (f.prod_lift g x).dom) :
(f.prod_lift g x).get h = ((f x).get _, (g x).get _)
@[simp]
theorem pfun.prod_lift_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) :
f.prod_lift g x = {dom := (f x).dom (g x).dom, get := λ (h : (f x).dom (g x).dom), ((f x).get _, (g x).get _)}
theorem pfun.mem_prod_lift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
y f.prod_lift g x y.fst f x y.snd g x
def pfun.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
α × β →. γ × δ

Product of partial functions.

Equations
@[simp]
theorem pfun.dom_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
(f.prod_map g).dom = {x : α × β | (f x.fst).dom (g x.snd).dom}
theorem pfun.get_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) (h : (f.prod_map g x).dom) :
(f.prod_map g x).get h = ((f x.fst).get _, (g x.snd).get _)
@[simp]
theorem pfun.prod_map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) :
f.prod_map g x = {dom := (f x.fst).dom (g x.snd).dom, get := λ (h : (f x.fst).dom (g x.snd).dom), ((f x.fst).get _, (g x.snd).get _)}
theorem pfun.mem_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} :
y f.prod_map g x y.fst f x.fst y.snd g x.snd
@[simp]
theorem pfun.prod_lift_fst_comp_snd_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
@[simp]
theorem pfun.prod_map_id_id {α : Type u_1} {β : Type u_2} :
(pfun.id α).prod_map (pfun.id β) = pfun.id × β)
@[simp]
theorem pfun.prod_map_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₁).prod_map (g₂.comp g₁) = (f₂.prod_map g₂).comp (f₁.prod_map g₁)