mathlib3 documentation

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 #

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:

source
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
source
@[protected, instance]
def pfun.inhabited {α : Type u_1} {β : Type u_2} :
inhabited (α →. β)
Equations
source
def pfun.dom {α : Type u_1} {β : Type u_2} (f : α →. β) :
set α

The domain of a partial function

Equations
source
@[simp]
theorem pfun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x ∈ f.dom ↔ ∃ (y : β), y ∈ f x
source
@[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}
source
theorem pfun.dom_eq {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.dom = {x : α | ∃ (y : β), y ∈ f x}
source
def pfun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
f.dom a → β

Evaluate a partial function

Equations
source
@[simp]
theorem pfun.fn_apply {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
f.fn a = (f a).get
source
def pfun.eval_opt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : decidable_pred (λ (_x : α), _x ∈ f.dom)] (x : α) :
option β

Evaluate a partial function to return an option

Equations
source
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

source
theorem pfun.ext {α : Type u_1} {β : Type u_2} {f g : α →. β} (H : ∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a) :
f = g
source
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
source
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
source
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
source
@[protected]
def pfun.lift {α : Type u_1} {β : Type u_2} (f : α → β) :
α →. β

Turn a total function into a partial function.

Equations
source
@[protected, instance]
def pfun.has_coe {α : Type u_1} {β : Type u_2} :
has_coe (α → β) (α →. β)
Equations
source
@[simp]
theorem pfun.lift_eq_coe {α : Type u_1} {β : Type u_2} (f : α → β) :
pfun.lift f = ↑f
source
@[simp]
theorem pfun.coe_val {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
↑f a = part.some (f a)
source
@[simp]
theorem pfun.dom_coe {α : Type u_1} {β : Type u_2} (f : α → β) :
↑f.dom = set.univ
source
theorem pfun.coe_injective {α : Type u_1} {β : Type u_2} :
function.injective coe
source
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
source
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
source
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
source
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
source
@[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
source
def pfun.res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
α →. β

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

Equations
source
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
source
theorem pfun.res_univ {α : Type u_1} {β : Type u_2} (f : α → β) :
pfun.res f set.univ = ↑f
source
theorem pfun.dom_iff_graph {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
x ∈ f.dom ↔ ∃ (y : β), (x, y) ∈ f.graph
source
theorem pfun.lift_graph {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} :
(a, b) ∈ ↑f.graph ↔ f a = b
source
@[protected]
def pfun.pure {α : Type u_1} {β : Type u_2} (x : β) :
α →. β

The monad pure function, the total constant x function

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

The monad map function, pointwise part.map

Equations
source
@[protected, instance]
def pfun.monad {α : Type u_1} :
monad (pfun α)
Equations
source
@[protected, instance]
def pfun.is_lawful_monad {α : Type u_1} :
is_lawful_monad (pfun α)
source
theorem pfun.pure_defined {α : Type u_1} {β : Type u_2} (p : set α) (x : β) :
p ⊆ (pfun.pure x).dom
source
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
source
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
source
theorem pfun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β} (h : b ∈ f.fix a) :
(f a).dom
source
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'
source
theorem pfun.fix_stop {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a : α} (hb : sum.inl b ∈ f a) :
b ∈ f.fix a

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

source
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'

source
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'
source
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
source
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') :
pfun.fix_induction h H = H a h (λ (a' : α) (h' : sum.inr a' ∈ f a), pfun.fix_induction _ H)
source
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 : α), sum.inl b ∈ 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
source
theorem pfun.fix_induction'_stop {α : Type u_1} {β : Type u_2} {C : α → Sort u_3} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ f.fix a) (fa : sum.inl b ∈ f a) (hbase : Π (a_final : α), sum.inl b ∈ f a_final → C a_final) (hind : Π (a₀ a₁ : α), b ∈ f.fix a₁ → sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) :
pfun.fix_induction' h hbase hind = hbase a fa
source
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 : α), sum.inl b ∈ f a_final → C a_final) (hind : Π (a₀ a₁ : α), b ∈ f.fix a₁ → sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) :
pfun.fix_induction' h hbase hind = hind a a' h' fa (pfun.fix_induction' h' hbase hind)
source
def pfun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
set β

Image of a set under a partial function.

Equations
source
theorem pfun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set α) :
f.image s = {y : β | ∃ (x : α) (H : x ∈ s), y ∈ f x}
source
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
source
theorem pfun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set α} (h : s ⊆ t) :
f.image s ⊆ f.image t
source
theorem pfun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set α) :
f.image (s ∩ t) ⊆ f.image s ∩ f.image t
source
theorem pfun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set α) :
f.image (s ∪ t) = f.image s ∪ f.image t
source
def pfun.preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
set α

Preimage of a set under a partial function.

Equations
source
theorem pfun.preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s = {x : α | ∃ (y : β) (H : y ∈ s), y ∈ f x}
source
@[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
source
theorem pfun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s ⊆ f.dom
source
theorem pfun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set β} (h : s ⊆ t) :
f.preimage s ⊆ f.preimage t
source
theorem pfun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.preimage (s ∩ t) ⊆ f.preimage s ∩ f.preimage t
source
theorem pfun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.preimage (s ∪ t) = f.preimage s ∪ f.preimage t
source
theorem pfun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
f.preimage set.univ = f.dom
source
theorem pfun.coe_preimage {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
↑f.preimage s = f ⁻¹' s
source
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
source
theorem pfun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.core s = {x : α | ∀ (y : β), y ∈ f x → y ∈ s}
source
@[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
source
theorem pfun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.domᶜ ⊆ f.core s
source
theorem pfun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : set β} (h : s ⊆ t) :
f.core s ⊆ f.core t
source
theorem pfun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : set β) :
f.core (s ∩ t) = f.core s ∩ f.core t
source
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
source
theorem pfun.core_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (t : set β) :
(pfun.res f s).core t = sᶜ ∪ f ⁻¹' t
source
theorem pfun.core_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : set β) :
↑f.core s = f ⁻¹' s
source
theorem pfun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s ⊆ f.core s
source
theorem pfun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.preimage s = f.core s ∩ f.dom
source
theorem pfun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.core s = f.preimage s ∪ f.domᶜ
source
theorem pfun.preimage_as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : set β) :
f.as_subtype ⁻¹' s = subtype.val ⁻¹' f.preimage s
source
def pfun.to_subtype {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β) :
α →. subtype p

Turns a function into a partial function to a subtype.

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

The identity as a partial function

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

Composition of partial functions as a partial function.

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

Product of partial functions.

Equations
source
@[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}
source
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 _)
source
@[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 _)}
source
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
source
def pfun.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
α × β →. γ × δ

Product of partial functions.

Equations
source
@[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}
source
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 _)
source
@[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 _)}
source
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
source
@[simp]
theorem pfun.prod_lift_fst_comp_snd_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
(f.comp ↑prod.fst).prod_lift (g.comp ↑prod.snd) = f.prod_map g
source
@[simp]
theorem pfun.prod_map_id_id {α : Type u_1} {β : Type u_2} :
(pfun.id α).prod_map (pfun.id β) = pfun.id (α × β)
source
@[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₁)