mathlib docs: data.pfun

structure roption :

Type u → Type 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.

source

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

option α

Convert an roption α with a decidable domain to an option

Equations

o.to_option = dite o.dom (λ (h : o.dom), option.some (o.get h)) (λ (h : ¬o.dom), option.none)

source

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

source

@[simp]

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

{dom := o.dom, get := λ (h : o.dom), o.get h} = o

roption eta expansion

source

def roption.mem {α : Type u_1} :

α → roption α → Prop

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

Equations

roption.mem a o = ∃ (h : o.dom), o.get h = a

source

@[instance]

def roption.has_mem {α : Type u_1} :

has_mem α (roption α)

Equations

roption.has_mem = {mem := roption.mem α}

source

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

a ∈ o = ∃ (h : o.dom), o.get h = a

source

theorem roption.dom_iff_mem {α : Type u_1} {o : roption α} :

o.dom ↔ ∃ (y : α), y ∈ o

source

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

o.get h ∈ o

source

theorem roption.ext {α : Type u_1} {o p : roption α} :

(∀ (a : α), a ∈ o ↔ a ∈ p) → o = p

roption extensionality

source

def roption.none {α : Type u_1} :

roption α

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

Equations

roption.none = {dom := false, get := false.rec α}

source

@[instance]

def roption.inhabited {α : Type u_1} :

inhabited (roption α)

Equations

roption.inhabited = {default := roption.none α}

source

@[simp]

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

a ∉ roption.none

source

def roption.some {α : Type u_1} :

α → roption α

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

Equations

roption.some a = {dom := true, get := λ (_x : true), a}

source

theorem roption.mem_unique {α : Type u_1} :

relator.left_unique has_mem.mem

source

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

o.get h' = a

source

@[simp]

theorem roption.get_some {α : Type u_1} {a : α} (ha : (roption.some a).dom) :

(roption.some a).get ha = a

source

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

a ∈ roption.some a

source

@[simp]

theorem roption.mem_some_iff {α : Type u_1} {a b : α} :

b ∈ roption.some a ↔ b = a

source

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

o = roption.some a ↔ a ∈ o

source

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

o = roption.none ↔ ∀ (a : α), a ∉ o

source

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

o = roption.none ↔ ¬o.dom

source

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

roption.some x ≠ roption.none

source

theorem roption.ne_none_iff {α : Type u_1} {o : roption α} :

o ≠ roption.none ↔ ∃ (x : α), o = roption.some x

source

@[simp]

theorem roption.some_inj {α : Type u_1} {a b : α} :

roption.some a = roption.some b ↔ a = b

source

@[simp]

theorem roption.some_get {α : Type u_1} {a : roption α} (ha : a.dom) :

roption.some (a.get ha) = a

source

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

a.get ha = b ↔ a = roption.some b

source

@[instance]

def roption.none_decidable {α : Type u_1} :

decidable roption.none.dom

Equations

roption.none_decidable = decidable.false

source

@[instance]

def roption.some_decidable {α : Type u_1} (a : α) :

decidable (roption.some a).dom

Equations

roption.some_decidable a = decidable.true

source

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

α → α

Equations

a.get_or_else d = dite a.dom (λ (ha : a.dom), a.get ha) (λ (ha : ¬a.dom), d)

source

@[simp]

theorem roption.get_or_else_none {α : Type u_1} (d : α) :

roption.none.get_or_else d = d

source

@[simp]

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

(roption.some a).get_or_else d = a

source

@[simp]

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

a ∈ o.to_option ↔ a ∈ o

source

def roption.of_option {α : Type u_1} :

option α → roption α

Convert an option α into an roption α

Equations

source

@[simp]

theorem roption.mem_of_option {α : Type u_1} {a : α} {o : option α} :

a ∈ roption.of_option o ↔ a ∈ o

source

@[simp]

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

(roption.of_option o).dom ↔ ↥(o.is_some)

source

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

roption.of_option o = {dom := ↥(o.is_some), get := option.get o}

source

@[instance]

def roption.has_coe {α : Type u_1} :

has_coe (option α) (roption α)

Equations

roption.has_coe = {coe := roption.of_option α}

source

@[simp]

theorem roption.mem_coe {α : Type u_1} {a : α} {o : option α} :

a ∈ ↑o ↔ a ∈ o

source

@[simp]

theorem roption.coe_none {α : Type u_1} :

↑option.none = roption.none

source

@[simp]

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

↑(option.some a) = roption.some a

source

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

P roption.none → (∀ (a : α), P (roption.some a)) → P a

source

@[instance]

def roption.of_option_decidable {α : Type u_1} (o : option α) :

decidable (roption.of_option o).dom

Equations

source

@[simp]

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

(roption.of_option o).to_option = o

source

@[simp]

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

roption.of_option o.to_option = o

source

def roption.equiv_option {α : Type u_1} :

roption α ≃ option α

Equations

roption.equiv_option = {to_fun := λ (o : roption α), o.to_option, inv_fun := roption.of_option α, left_inv := _, right_inv := _}

source

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

roption.assert p f = {dom := ∃ (h : p), (f h).dom, get := λ (ha : ∃ (h : p), (f h).dom), (f _).get _}

source

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

f.bind g = roption.assert f.dom (λ (b : f.dom), g (f.get b))

source

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

roption.map f o = {dom := o.dom, get := f ∘ o.get}

source

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

a ∈ o → f a ∈ roption.map f o

source

@[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

source

@[simp]

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

roption.map f roption.none = roption.none

source

@[simp]

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

roption.map f (roption.some a) = roption.some (f a)

source

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

a ∈ f h → a ∈ roption.assert p f

source

@[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

source

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

a ∈ f → b ∈ g a → b ∈ f.bind g

source

@[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

source

@[simp]

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

roption.none.bind f = roption.none

source

@[simp]

theorem roption.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → roption β) :

(roption.some a).bind f = f a

source

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

x.bind (roption.some ∘ f) = roption.map f x

source

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)

source

@[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))

source

@[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))

source

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

roption.map g (roption.map f o) = roption.map (g ∘ f) o

source

@[instance]

def roption.monad :

monad roption

Equations

roption.monad = monad.mk

source

@[instance]

def roption.is_lawful_monad :

is_lawful_monad roption

Equations

roption.is_lawful_monad = _

source

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

roption.map f o = o

source

@[simp]

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

x.bind roption.some = x

source

@[simp]

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

has_pure.pure a = roption.some a

source

@[simp]

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

return a = roption.some a

source

@[simp]

theorem roption.map_eq_map {α β : Type u_1} (f : α → β) (o : roption α) :

f <$> o = roption.map f o

source

@[simp]

theorem roption.bind_eq_bind {α β : Type u_1} (f : roption α) (g : α → roption β) :

f >>= g = f.bind g

source

@[instance]

def roption.monad_fail :

monad_fail roption

Equations

roption.monad_fail = {fail := λ (_x : Type u_1) (_x_1 : string), roption.none}

source

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

(p → o.dom) → roption α

Equations

roption.restrict p {dom := d, get := f} H = {dom := p, get := λ (h : p), f _}

source

@[simp]

theorem roption.mem_restrict {α : Type u_1} (p : Prop) (o : roption α) (h : p → o.dom) (a : α) :

a ∈ roption.restrict p o h ↔ p ∧ a ∈ o

source

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

roption α → α

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

source

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

(f h).dom → (roption.assert p f).dom

source

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

source

@[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

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

Equations

(α →. β) = (α → roption β)

source

@[instance]

def pfun.inhabited {α : Type u_1} {β : Type u_2} :

inhabited (α →. β)

Equations

pfun.inhabited = {default := λ (a : α), roption.none}

source

def pfun.dom {α : Type u_1} {β : Type u_2} :

(α →. β) → set α

The domain of a partial function

Equations

f.dom = {a : α | (f a).dom}

source

theorem pfun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :

x ∈ f.dom ↔ ∃ (y : β), y ∈ f 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 : α →. β) (x : α) :

f.dom x → β

Evaluate a partial function

Equations

f.fn x h = (f x).get h

source

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

f.eval_opt x = (f x).to_option

source

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

source

theorem pfun.ext {α : Type u_1} {β : Type u_2} {f g : α →. β} :

(∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a) → f = g

source

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

f.as_subtype s = f.fn ↑s _

source

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

pfun.equiv_subtype = {to_fun := λ (f : α →. β), ⟨λ (a : α), (f a).dom, f.as_subtype⟩, inv_fun := λ (f : Σ (p : α → Prop), subtype p → β) (x : α), {dom := f.fst x, get := λ (h : f.fst x), f.snd ⟨x, h⟩}, left_inv := _, right_inv := _}

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

def pfun.lift {α : Type u_1} {β : Type u_2} :

(α → β) → α →. β

Turn a total function into a partial function

Equations

pfun.lift f = λ (a : α), roption.some (f a)

source

@[instance]

def pfun.has_coe {α : Type u_1} {β : Type u_2} :

has_coe (α → β) (α →. β)

Equations

pfun.has_coe = {coe := pfun.lift β}

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

source

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

f.graph = {p : α × β | p.snd ∈ f p.fst}

source

def pfun.graph' {α : Type u_1} {β : Type u_2} :

(α →. β) → rel α β

Equations

f.graph' = λ (x : α) (y : β), y ∈ f x

source

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}

source

def pfun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : set α} :

p ⊆ f.dom → α →. β

Restrict a partial function to a smaller domain.

Equations

f.restrict H = λ (x : α), roption.restrict (p x) (f x) H

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} :

(α → β) → set α → α →. β

Equations

pfun.res f s = (pfun.lift f).restrict _

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

def pfun.pure {α : Type u_1} {β : Type u_2} :

β → α →. β

The monad pure function, the total constant x function

Equations

pfun.pure x = λ (_x : α), roption.some x

source

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)

source

def pfun.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} :

(β → γ) → (α →. β) → α →. γ

The monad map function, pointwise roption.map

Equations

pfun.map f g = λ (a : α), roption.map f (g a)

source

@[instance]

def pfun.monad {α : Type u_1} :

monad (pfun α)

Equations

pfun.monad = monad.mk

source

@[instance]

def pfun.is_lawful_monad {α : Type u_1} :

is_lawful_monad (pfun α)

Equations

pfun.is_lawful_monad = _

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

p ⊆ f.dom → (∀ (x : β), p ⊆ (g x).dom) → p ⊆ (f >>= g).dom

source

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

(α →. β ⊕ α) → α →. β

Equations

f.fix = λ (a : α), roption.assert (acc (λ (x y : α), sum.inr x ∈ f y) a) (λ (h : acc (λ (x y : α), sum.inr x ∈ f y) a), well_founded.fix_F (λ (a : α) (IH : Π (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → roption β), roption.assert (f a).dom (λ (hf : (f a).dom), (λ (_x : β ⊕ α) (e : (f a).get hf = _x), _x.cases_on (λ (b : β) (e : (f a).get hf = sum.inl b), roption.some b) (λ (a' : α) (e : (f a).get hf = sum.inr a'), IH a' _) e) ((f a).get hf) _)) a h)

source

theorem pfun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β} :

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

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 a → C a') → C a) → C a

Equations

pfun.fix_induction h H = acc.drec (λ (a : α) (ha : ∀ (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → acc (λ (x y : α), sum.inr x ∈ f y) y) (IH : Π (y : α) (a : (λ (x y : α), sum.inr x ∈ f y) y a), (λ {a : α} (_x : acc (λ (x y : α), sum.inr x ∈ f y) a), (∃ (h : acc (λ (x y : α), sum.inr x ∈ f y) a), b ∈ well_founded.fix_F (λ (a : α) (IH : Π (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → roption β), roption.assert (f a).dom (λ (hf : (f a).dom), (λ (_x : β ⊕ α) (e : (f a).get hf = _x), _x.cases_on (λ (b : β) (e : (f a).get hf = sum.inl b), roption.some b) (λ (a' : α) (e : (f a).get hf = sum.inr a'), IH a' _) e) ((f a).get hf) _)) a h) → b ∈ well_founded.fix_F (λ (a : α) (IH : Π (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → roption β), roption.assert (f a).dom (λ (hf : (f a).dom), (λ (_x : β ⊕ α) (e : (f a).get hf = _x), _x.cases_on (λ (b : β) (e : (f a).get hf = sum.inl b), roption.some b) (λ (a' : α) (e : (f a).get hf = sum.inr a'), IH a' _) e) ((f a).get hf) _)) a _x → C a) _) (h : ∃ (h : acc (λ (x y : α), sum.inr x ∈ f y) a), b ∈ well_founded.fix_F (λ (a : α) (IH : Π (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → roption β), roption.assert (f a).dom (λ (hf : (f a).dom), (λ (_x : β ⊕ α) (e : (f a).get hf = _x), _x.cases_on (λ (b : β) (e : (f a).get hf = sum.inl b), roption.some b) (λ (a' : α) (e : (f a).get hf = sum.inr a'), IH a' _) e) ((f a).get hf) _)) a h) (h₂ : b ∈ well_founded.fix_F (λ (a : α) (IH : Π (y : α), (λ (x y : α), sum.inr x ∈ f y) y a → roption β), roption.assert (f a).dom (λ (hf : (f a).dom), (λ (_x : β ⊕ α) (e : (f a).get hf = _x), _x.cases_on (λ (b : β) (e : (f a).get hf = sum.inl b), roption.some b) (λ (a' : α) (e : (f a).get hf = sum.inr a'), IH a' _) e) ((f a).get hf) _)) a _), H a _ (λ (a' : α) (ha' : b ∈ f.fix a') (fa' : sum.inr a' ∈ f a), IH a' fa' _ _)) _ _ _

source

def pfun.image {α : Type u_1} {β : Type u_2} :

(α →. β) → set α → set β

Equations

f.image s = f.graph'.image s

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 α} :

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} :

(α →. β) → set β → set α

Equations

f.preimage s = rel.preimage (λ (x : α) (y : β), y ∈ f x) s

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

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 β} :

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

def pfun.core {α : Type u_1} {β : Type u_2} :

(α →. β) → set β → set α

Equations

f.core s = f.graph'.core s

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

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 β} :

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

mathlib documentation

data.pfun

General documentation

Additional documentation

Library

mathlib documentation

data.​pfun

General documentation

Additional documentation

Library

data.pfun