mathlib documentation

data.pfun

source
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
source
theorem roption.ext' {α : Type u_1} {o p : roption α} (H1 : o.dom ↔ p.dom) (H2 : ∀ (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} (a : α) (o : roption α) :
Prop

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

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

Equations
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
@[ext]
theorem roption.ext {α : Type u_1} {o p : roption α} (H : ∀ (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
source
@[instance]
def roption.inhabited {α : Type u_1} :
inhabited (roption α)

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

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

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

Equations
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
theorem roption.eq_none_or_eq_some {α : 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
source
@[instance]
def roption.some_decidable {α : Type u_1} (a : α) :
decidable (roption.some a).dom

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

Equations
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} (a : 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
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} :
↑none = roption.none

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

source
theorem roption.induction_on {α : Type u_1} {P : roption α → Prop} (a : roption α) (hnone : P roption.none) (hsome : ∀ (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
source
@[instance]
def roption.order_bot {α : Type u_1} :
order_bot (roption α)

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

Equations
source
theorem roption.le_total_of_le_of_le {α : Type u_1} {x y : roption α} (z : roption α) (hx : x ≤ z) (hy : y ≤ z) :
x ≤ y ∨ y ≤ x

source
def roption.assert {α : Type u_1} (p : Prop) (f : 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
source
def roption.bind {α : Type u_1} {β : Type u_2} (f : roption α) (g : α → roption β) :
roption β

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

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

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

Equations
source
theorem roption.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : roption α} {a : α} (a_1 : 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_1 : 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.assert_pos {α : Type u_1} {p : Prop} {f : p → roption α} (h : p) :
roption.assert p f = f h

source
theorem roption.assert_neg {α : Type u_1} {p : Prop} {f : p → roption α} (h : ¬p) :
roption.assert p f = roption.none

source
theorem roption.mem_bind {α : Type u_1} {β : Type u_2} {f : roption α} {g : α → roption β} {a : α} {b : β} (a_1 : a ∈ f) (a_2 : 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
source
@[instance]
def roption.is_lawful_monad  :
is_lawful_monad roption

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 : α) :
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
theorem roption.bind_le {β α : Type u_2} (x : roption α) (f : α → roption β) (y : roption β) :
x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

source
@[instance]
def roption.monad_fail  :
monad_fail roption

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

Equations
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} (o : 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) (a : (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) (a : (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
source
@[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
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 : α) (h : f.dom x) :
β

Evaluate a partial function

Equations
source
def pfun.eval_opt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : decidable_pred 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)) :
β

Turn a partial function into a function out of a subtype

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

Turn a total function into a partial function

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

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

The graph of a partial function is 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 α β

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

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
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 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} (f : β → γ) (g : α →. β) :
α →. γ

The monad map function, pointwise roption.map

Equations
source
@[instance]
def pfun.monad {α : Type u_1} :
monad (pfun α)

Equations
source
@[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 : α →. β ⊕ α) :
α →. β

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

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

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 α

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

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