mathlib documentation

data.pfun

structure roption  :
Type uType u
  • dom : Prop
  • get : c.dom → α

roption α is the type of "partial values" of type α. It is similar to option α except the domain condition can be an arbitrary proposition, not necessarily decidable.

def roption.to_option {α : Type u_1} (o : roption α) [decidable o.dom] :

Convert an roption α with a decidable domain to an option

Equations
theorem roption.ext' {α : Type u_1} {o p : roption α} :
(o.dom p.dom)(∀ (h₁ : o.dom) (h₂ : p.dom), o.get h₁ = p.get h₂)o = p

roption extensionality

@[simp]
theorem roption.eta {α : Type u_1} (o : roption α) :
{dom := o.dom, get := λ (h : o.dom), o.get h} = o

roption eta expansion

def roption.mem {α : Type u_1} :
α → roption α → Prop

a ∈ o means that o is defined and equal to a

Equations
@[instance]
def roption.has_mem {α : Type u_1} :

Equations
theorem roption.mem_eq {α : Type u_1} (a : α) (o : roption α) :
a o = ∃ (h : o.dom), o.get h = a

theorem roption.dom_iff_mem {α : Type u_1} {o : roption α} :
o.dom ∃ (y : α), y o

theorem roption.get_mem {α : Type u_1} {o : roption α} (h : o.dom) :
o.get h o

@[ext]
theorem roption.ext {α : Type u_1} {o p : roption α} :
(∀ (a : α), a o a p)o = p

roption extensionality

def roption.none {α : Type u_1} :

The none value in roption has a false domain and an empty function.

Equations
@[instance]
def roption.inhabited {α : Type u_1} :

Equations
@[simp]
theorem roption.not_mem_none {α : Type u_1} (a : α) :

def roption.some {α : Type u_1} :
α → roption α

The some a value in roption has a true domain and the function returns a.

Equations
theorem roption.get_eq_of_mem {α : Type u_1} {o : roption α} {a : α} (h : a o) (h' : o.dom) :
o.get h' = a

@[simp]
theorem roption.get_some {α : Type u_1} {a : α} (ha : (roption.some a).dom) :
(roption.some a).get ha = a

theorem roption.mem_some {α : Type u_1} (a : α) :

@[simp]
theorem roption.mem_some_iff {α : Type u_1} {a b : α} :

theorem roption.eq_some_iff {α : Type u_1} {a : α} {o : roption α} :

theorem roption.eq_none_iff {α : Type u_1} {o : roption α} :
o = roption.none ∀ (a : α), a o

theorem roption.eq_none_iff' {α : Type u_1} {o : roption α} :

theorem roption.some_ne_none {α : Type u_1} (x : α) :

theorem roption.ne_none_iff {α : Type u_1} {o : roption α} :
o roption.none ∃ (x : α), o = roption.some x

theorem roption.eq_none_or_eq_some {α : Type u_1} (o : roption α) :
o = roption.none ∃ (x : α), o = roption.some x

@[simp]
theorem roption.some_inj {α : Type u_1} {a b : α} :

@[simp]
theorem roption.some_get {α : Type u_1} {a : roption α} (ha : a.dom) :
roption.some (a.get ha) = a

theorem roption.get_eq_iff_eq_some {α : Type u_1} {a : roption α} {ha : a.dom} {b : α} :
a.get ha = b a = roption.some b

@[instance]
def roption.some_decidable {α : Type u_1} (a : α) :

Equations
def roption.get_or_else {α : Type u_1} (a : roption α) [decidable a.dom] :
α → α

Equations
@[simp]
theorem roption.get_or_else_none {α : Type u_1} (d : α) :

@[simp]
theorem roption.get_or_else_some {α : Type u_1} (a d : α) :

@[simp]
theorem roption.mem_to_option {α : Type u_1} {o : roption α} [decidable o.dom] {a : α} :

def roption.of_option {α : Type u_1} :
option αroption α

Convert an option α into an roption α

Equations
@[simp]
theorem roption.mem_of_option {α : Type u_1} {a : α} {o : option α} :

@[simp]
theorem roption.of_option_dom {α : Type u_1} (o : option α) :

theorem roption.of_option_eq_get {α : Type u_1} (o : option α) :

@[instance]
def roption.has_coe {α : Type u_1} :

Equations
@[simp]
theorem roption.mem_coe {α : Type u_1} {a : α} {o : option α} :
a o a o

@[simp]
theorem roption.coe_none {α : Type u_1} :

@[simp]
theorem roption.coe_some {α : Type u_1} (a : α) :

theorem roption.induction_on {α : Type u_1} {P : roption α → Prop} (a : roption α) :
P roption.none(∀ (a : α), P (roption.some a))P a

@[simp]
theorem roption.to_of_option {α : Type u_1} (o : option α) :

@[simp]
theorem roption.of_to_option {α : Type u_1} (o : roption α) [decidable o.dom] :

def roption.equiv_option {α : Type u_1} :

Equations
@[instance]
def roption.order_bot {α : Type u_1} :

Equations
@[instance]
def roption.preorder {α : Type u_1} :

Equations
theorem roption.le_total_of_le_of_le {α : Type u_1} {x y : roption α} (z : roption α) :
x zy zx y y x

def roption.assert {α : Type u_1} (p : Prop) :
(p → roption α)roption α

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

Equations
def roption.bind {α : Type u_1} {β : Type u_2} :
roption α(α → roption β)roption β

The bind operation has value g (f.get), and is defined when all the parts are defined.

Equations
def roption.map {α : Type u_1} {β : Type u_2} :
(α → β)roption αroption β

The map operation for roption just maps the value and maintains the same domain.

Equations
theorem roption.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : roption α} {a : α} :
a of a roption.map f o

@[simp]
theorem roption.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : roption α} {b : β} :
b roption.map f o ∃ (a : α) (H : a o), f a = b

@[simp]
theorem roption.map_none {α : Type u_1} {β : Type u_2} (f : α → β) :

@[simp]
theorem roption.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :

theorem roption.mem_assert {α : Type u_1} {p : Prop} {f : p → roption α} {a : α} (h : p) :
a f ha roption.assert p f

@[simp]
theorem roption.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → roption α} {a : α} :
a roption.assert p f ∃ (h : p), a f h

theorem roption.assert_pos {α : Type u_1} {p : Prop} {f : p → roption α} (h : p) :

theorem roption.assert_neg {α : Type u_1} {p : Prop} {f : p → roption α} :

theorem roption.mem_bind {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} {a : α} {b : β} :
a fb g ab f.bind g

@[simp]
theorem roption.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} {b : β} :
b f.bind g ∃ (a : α) (H : a f), b g a

@[simp]
theorem roption.bind_none {α : Type u_1} {β : Type u_2} (f : α → roption β) :

@[simp]
theorem roption.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → roption β) :
(roption.some a).bind f = f a

theorem roption.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : roption α) :

theorem roption.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : roption α) (g : α → roption β) (k : β → roption γ) :
(f.bind g).bind k = f.bind (λ (x : α), (g x).bind k)

@[simp]
theorem roption.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (x : roption α) (g : β → roption γ) :
(roption.map f x).bind g = x.bind (λ (y : α), g (f y))

@[simp]
theorem roption.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → roption β) (x : roption α) (g : β → γ) :
roption.map g (x.bind f) = x.bind (λ (y : α), roption.map g (f y))

theorem roption.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : roption α) :

@[instance]

Equations
theorem roption.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : roption α) :

@[simp]
theorem roption.bind_some_right {α : Type u_1} (x : roption α) :

@[simp]
theorem roption.pure_eq_some {α : Type u_1} (a : α) :

@[simp]
theorem roption.ret_eq_some {α : Type u_1} (a : α) :

@[simp]
theorem roption.map_eq_map {α β : Type u_1} (f : α → β) (o : roption α) :
f <$> o = roption.map f o

@[simp]
theorem roption.bind_eq_bind {α β : Type u_1} (f : roption α) (g : α → roption β) :
f >>= g = f.bind g

theorem roption.bind_le {β α : Type u_2} (x : roption α) (f : α → roption β) (y : roption β) :
x >>= f y ∀ (a : α), a xf a y

@[instance]

Equations
def roption.restrict {α : Type u_1} (p : Prop) (o : roption α) :
(p → o.dom)roption α

Equations
@[simp]
theorem roption.mem_restrict {α : Type u_1} (p : Prop) (o : roption α) (h : p → o.dom) (a : α) :

meta def roption.unwrap {α : Type u_1} :
roption α → α

unwrap o gets the value at o, ignoring the condition. (This function is unsound.)

theorem roption.assert_defined {α : Type u_1} {p : Prop} {f : p → roption α} (h : p) :
(f h).dom(roption.assert p f).dom

theorem roption.bind_defined {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} (h : f.dom) :
(g (f.get h)).dom(f.bind g).dom

@[simp]
theorem roption.bind_dom {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} :
(f.bind g).dom ∃ (h : f.dom), (g (f.get h)).dom

def pfun  :
Type u_1Type u_2Type (max u_1 u_2)

pfun α β, or α →. β, is the type of partial functions from α to β. It is defined as α → roption β.

Equations
@[instance]
def pfun.inhabited {α : Type u_1} {β : Type u_2} :
inhabited →. β)

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

Evaluate a partial function

Equations
def pfun.eval_opt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : decidable_pred f.dom] :
α → option β

Evaluate a partial function to return an option

Equations
theorem pfun.ext' {α : Type u_1} {β : Type u_2} {f g : α →. β} :
(∀ (a : α), a f.dom a g.dom)(∀ (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 : α →. β} :
(∀ (a : α) (b : β), b f a b g a)f = g

def pfun.as_subtype {α : Type u_1} {β : Type u_2} (f : α →. β) :
(f.dom) → β

Turn a partial function into a function out of a subtype

Equations
def pfun.equiv_subtype {α : Type u_1} {β : Type u_2} :
→. β) Σ (p : α → Prop), subtype p → β

The set of partial functions α →. β is equivalent to the set 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} :
(α → β)α →. β

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 = roption.some (f a)

def pfun.graph {α : Type u_1} {β : Type u_2} :
→. β)set × β)

The graph of a partial function is 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} :
→. β)rel α β

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

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

The monad pure function, the total constant x function

Equations
def pfun.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
→. β)(β → α →. γ)α →. γ

The monad bind function, pointwise roption.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} :
(β → γ)→. β)α →. γ

The monad map function, pointwise roption.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 : β → α →. γ} :
p f.dom(∀ (x : β), p (g x).dom)p (f >>= g).dom

def pfun.fix {α : Type u_1} {β : Type u_2} :
→. β α)α →. β

Equations
theorem pfun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} :
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 : α} :
b f.fix a(Π (a : α), b f.fix a(Π (a' : α), b f.fix a'sum.inr a' f aC a')C a)C a

Equations
def pfun.image {α : Type u_1} {β : Type u_2} :
→. β)set αset β

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 α} :
s tf.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} :
→. β)set βset α

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 β} :
s tf.preimage s f.preimage 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} :
→. β)set βset α

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 β} :
s tf.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 β) :