mathlib documentation

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 #

Partial functions as relations #

Partial functions can be considered as relations, so we specialize some rel definitions to pfun:

pfun α as a monad #

Monad operations:

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
@[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
theorem pfun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x f.dom ∃ (y : β), y f 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 : α →. β) (x : α) (h : f.dom x) :
β

Evaluate a partial function

Equations
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), subtype p → β

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
def pfun.lift {α : Type u_1} {β : Type u_2} (f : α → β) :
α →. β

Turn a total function into a partial function.

Equations
@[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 : α → β) :
@[simp]
theorem pfun.coe_val {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
f a = part.some (f a)
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 pfun.res f 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
def pfun.pure {α : Type u_1} {β : Type u_2} (x : β) :
α →. β

The monad pure function, the total constant x function

Equations
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)
def pfun.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (g : α →. β) :
α →. γ

The monad map function, pointwise part.map

Equations
@[instance]
def pfun.monad {α : Type u_1} :
monad (pfun α)
Equations
@[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 sum.inl b f a ∃ (a' : α), sum.inr a' f a b 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' : α), b f.fix a'sum.inr a' f aC a')C a) :
C a

A recursion principle for pfun.fix.

Equations
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}
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 : α →. β) :
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}
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 β) :