data.pfun

# 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.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
• f.ran = {b : β | ∃ (a : α), b f a}
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 : α →. β α} (a : α) {b : β} (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 {α : 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'

def pfun.fix_induction {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {C : α → Sort u_3} {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
def pfun.fix_induction' {α : Type u_1} {β : Type u_2} (f : α →. β α) (b : β) {C : α → Sort u_3} {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
• h 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 _) _)
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 xy s}
@[simp]
theorem pfun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : set β) :
x f.core s ∀ (y : β), y f xy 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 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 β) :
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