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

• PFun α β: Type of partial functions from α to β. Defined as α → Part β and denoted α →. β.
• PFun.Dom: Domain of a partial function. Set of values on which it is defined. Not to be confused with the domain of a function α → β, which is a type (α presently).
• PFun.fn: Evaluation of a partial function. Takes in an element and a proof it belongs to the partial function's Dom.
• PFun.asSubtype: Returns a partial function as a function from its Dom.
• PFun.toSubtype: Restricts the codomain of a function to a subtype.
• PFun.evalOpt: Returns a partial function with a decidable Dom as a function a → Option β.
• PFun.lift: Turns a function into a partial function.
• PFun.id: The identity as a partial function.
• PFun.comp: Composition of partial functions.
• PFun.restrict: Restriction of a partial function to a smaller Dom.
• PFun.res: Turns a function into a partial function with a prescribed domain.
• PFun.fix : First return map of a partial function f : α →. β ⊕ α.
• PFun.fix_induction: A recursion principle for PFun.fix.

Partial functions as relations

Partial functions can be considered as relations, so we specialize some Rel definitions to PFun:

• PFun.image: Image of a set under a partial function.
• PFun.ran: Range of a partial function.
• PFun.preimage: Preimage of a set under a partial function.
• PFun.core: Core of a set under a partial function.
• PFun.graph: Graph of a partial function a →. βas a Set (α × β).
• PFun.graph': Graph of a partial function a →. βas a Rel α β.

PFun α as a monad

Monad operations:

• PFun.pure: The monad pure function, the constant x function.
• PFun.bind: The monad bind function, pointwise Part.bind
• PFun.map: The monad map function, pointwise Part.map.

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

• (α →. β) = (α → Part β)

def «term_→._» : Lean.TrailingParserDescr

α →. β is notation for the type PFun α β of partial functions from α to β.

Equations

• «term_→._» = Lean.ParserDescr.trailingNode `term_→._ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →. ") (Lean.ParserDescr.cat `term 25))

instance PFun.inhabited {α : Type u_1} {β : Type u_2} : Inhabited (α →. β)

Equations

• PFun.inhabited = { default := fun (x : α) => Part.none }

def PFun.Dom {α : Type u_1} {β : Type u_2} (f : α →. β) : Set α

The domain of a partial function

Equations

• PFun.Dom f = {a : α | (f a).Dom}

@[simp]

theorem PFun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) : x ∈ PFun.Dom f ↔ ∃ (y : β), y ∈ f x

@[simp]

theorem PFun.dom_mk {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : (a : α) → p a → β) : (PFun.Dom fun (x : α) => { Dom := p x, get := f x }) = {x : α | p x}

theorem PFun.dom_eq {α : Type u_1} {β : Type u_2} (f : α →. β) : PFun.Dom f = {x : α | ∃ (y : β), y ∈ f x}

def PFun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) : PFun.Dom f a → β

Evaluate a partial function

Equations

• PFun.fn f a = (f a).get

@[simp]

theorem PFun.fn_apply {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) : PFun.fn f a = (f a).get

def PFun.evalOpt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : DecidablePred fun (x : α) => x ∈ PFun.Dom f] (x : α) : Option β

Evaluate a partial function to return an Option

Equations

• PFun.evalOpt f x = Part.toOption (f x)

theorem PFun.ext' {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H1 : ∀ (a : α), a ∈ PFun.Dom f ↔ a ∈ PFun.Dom g) (H2 : ∀ (a : α) (p : PFun.Dom f a) (q : PFun.Dom g a), PFun.fn f a p = PFun.fn g 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.asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : ↑(PFun.Dom f)) : β

Turns a partial function into a function out of its domain.

Equations

• PFun.asSubtype f s = PFun.fn f ↑s (_ : ↑s ∈ PFun.Dom f)

def PFun.equivSubtype {α : 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

• One or more equations did not get rendered due to their size.

theorem PFun.asSubtype_eq_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β} (fxy : y ∈ f x) (domx : x ∈ PFun.Dom f) : PFun.asSubtype f { val := x, property := domx } = y

def PFun.lift {α : Type u_1} {β : Type u_2} (f : α → β) : α →. β

Turn a total function into a partial function.

Equations

• ↑f a = Part.some (f a)

instance PFun.coe {α : Type u_1} {β : Type u_2} : Coe (α → β) (α →. β)

Equations

• PFun.coe = { coe := PFun.lift }

@[simp]

theorem PFun.coe_val {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : ↑f a = Part.some (f a)

@[simp]

theorem PFun.dom_coe {α : Type u_1} {β : Type u_2} (f : α → β) : PFun.Dom ↑f = Set.univ

theorem PFun.lift_injective {α : Type u_1} {β : Type u_2} : Function.Injective PFun.lift

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

• PFun.graph f = {p : α × β | p.2 ∈ f p.1}

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

• PFun.graph' f x y = (y ∈ f x)

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

• PFun.ran f = {b : β | ∃ (a : α), b ∈ f a}

def PFun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : Set α} (H : p ⊆ PFun.Dom f) : α →. β

Restrict a partial function to a smaller domain.

Equations

• PFun.restrict f H x = Part.restrict (x ∈ p) (f x) (_ : x ∈ p → x ∈ PFun.Dom f)

@[simp]

theorem PFun.mem_restrict {α : Type u_1} {β : Type u_2} {f : α →. β} {s : Set α} (h : s ⊆ PFun.Dom f) (a : α) (b : β) : b ∈ PFun.restrict f 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

• PFun.res f s = PFun.restrict ↑f (_ : s ⊆ Set.univ)

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 : α → β) : PFun.res f Set.univ = ↑f

theorem PFun.dom_iff_graph {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) : x ∈ PFun.Dom f ↔ ∃ (y : β), (x, y) ∈ PFun.graph f

theorem PFun.lift_graph {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β} : (a, b) ∈ PFun.graph ↑f ↔ f a = b

def PFun.pure {α : Type u_1} {β : Type u_2} (x : β) : α →. β

The monad pure function, the total constant x function

Equations

• PFun.pure x✝ x = Part.some x✝

def PFun.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : β → α →. γ) : α →. γ

The monad bind function, pointwise Part.bind

Equations

• PFun.bind f g a = Part.bind (f a) fun (b : β) => g b a

@[simp]

theorem PFun.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : β → α →. γ) (a : α) : PFun.bind f g a = Part.bind (f a) fun (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

• PFun.map f g a = Part.map f (g a)

instance PFun.monad {α : Type u_1} : Monad (PFun α)

Equations

• PFun.monad = Monad.mk

instance PFun.lawfulMonad {α : Type u_1} : LawfulMonad (PFun α)

Equations

• (_ : LawfulMonad (PFun α)) = (_ : LawfulMonad (PFun α))

theorem PFun.pure_defined {α : Type u_1} {β : Type u_2} (p : Set α) (x : β) : p ⊆ PFun.Dom (PFun.pure x)

theorem PFun.bind_defined {α : Type u_7} {β : Type u_8} {γ : Type u_8} (p : Set α) {f : α →. β} {g : β → α →. γ} (H1 : p ⊆ PFun.Dom f) (H2 : ∀ (x : β), p ⊆ PFun.Dom (g x)) : p ⊆ PFun.Dom (f >>= g)

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

• One or more equations did not get rendered due to their size.

theorem PFun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β} (h : b ∈ PFun.fix f a) : (f a).Dom

theorem PFun.mem_fix_iff {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {b : β} : b ∈ PFun.fix f a ↔ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ PFun.fix f a'

theorem PFun.fix_stop {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a : α} (hb : Sum.inl b ∈ f a) : b ∈ PFun.fix f a

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

theorem PFun.fix_fwd_eq {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {a : α} {a' : α} (ha' : Sum.inr a' ∈ f a) : PFun.fix f a = PFun.fix f a'

If advancing one step from a on f leads to a' : α, then f.fix a = f.fix a'

theorem PFun.fix_fwd {α : Type u_1} {β : Type u_2} {f : α →. β ⊕ α} {b : β} {a : α} {a' : α} (hb : b ∈ PFun.fix f a) (ha' : Sum.inr a' ∈ f a) : b ∈ PFun.fix f a'

def PFun.fixInduction {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ PFun.fix f a) (H : (a' : α) → b ∈ PFun.fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a') : C a

A recursion principle for PFun.fix.

Equations

• One or more equations did not get rendered due to their size.

theorem PFun.fixInduction_spec {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ PFun.fix f a) (H : (a' : α) → b ∈ PFun.fix f a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a') : PFun.fixInduction h H = H a h fun (a' : α) (h' : Sum.inr a' ∈ f a) => PFun.fixInduction (_ : b ∈ PFun.fix f a') H

def PFun.fixInduction' {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ PFun.fix f a) (hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final) (hind : (a₀ a₁ : α) → b ∈ PFun.fix f 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

• One or more equations did not get rendered due to their size.

theorem PFun.fixInduction'_stop {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} (h : b ∈ PFun.fix f a) (fa : Sum.inl b ∈ f a) (hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final) (hind : (a₀ a₁ : α) → b ∈ PFun.fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) : PFun.fixInduction' h hbase hind = hbase a fa

theorem PFun.fixInduction'_fwd {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {f : α →. β ⊕ α} {b : β} {a : α} {a' : α} (h : b ∈ PFun.fix f a) (h' : b ∈ PFun.fix f a') (fa : Sum.inr a' ∈ f a) (hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final) (hind : (a₀ a₁ : α) → b ∈ PFun.fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) : PFun.fixInduction' h hbase hind = hind a a' h' fa (PFun.fixInduction' h' hbase hind)

def PFun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) : Set β

Image of a set under a partial function.

Equations

• PFun.image f s = Rel.image (PFun.graph' f) s

theorem PFun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) : PFun.image f s = {y : β | ∃ x ∈ s, y ∈ f x}

theorem PFun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : Set α) : y ∈ PFun.image f s ↔ ∃ x ∈ s, y ∈ f x

theorem PFun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set α} {t : Set α} (h : s ⊆ t) : PFun.image f s ⊆ PFun.image f t

theorem PFun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) : PFun.image f (s ∩ t) ⊆ PFun.image f s ∩ PFun.image f t

theorem PFun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) : PFun.image f (s ∪ t) = PFun.image f s ∪ PFun.image f t

def PFun.preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : Set α

Preimage of a set under a partial function.

Equations

• PFun.preimage f s = Rel.image (fun (x : β) (y : α) => x ∈ f y) s

theorem PFun.Preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.preimage f s = {x : α | ∃ y ∈ s, y ∈ f x}

@[simp]

theorem PFun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α) : x ∈ PFun.preimage f s ↔ ∃ y ∈ s, y ∈ f x

theorem PFun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.preimage f s ⊆ PFun.Dom f

theorem PFun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s ⊆ t) : PFun.preimage f s ⊆ PFun.preimage f t

theorem PFun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) : PFun.preimage f (s ∩ t) ⊆ PFun.preimage f s ∩ PFun.preimage f t

theorem PFun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) : PFun.preimage f (s ∪ t) = PFun.preimage f s ∪ PFun.preimage f t

theorem PFun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) : PFun.preimage f Set.univ = PFun.Dom f

theorem PFun.coe_preimage {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : PFun.preimage (↑f) s = f ⁻¹' s

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

• PFun.core f s = Rel.core (PFun.graph' f) s

theorem PFun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.core f s = {x : α | ∀ y ∈ f x, y ∈ s}

@[simp]

theorem PFun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : Set β) : x ∈ PFun.core f s ↔ ∀ y ∈ f x, y ∈ s

theorem PFun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : (PFun.Dom f)ᶜ ⊆ PFun.core f s

theorem PFun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s ⊆ t) : PFun.core f s ⊆ PFun.core f t

theorem PFun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) : PFun.core f (s ∩ t) = PFun.core f s ∩ PFun.core f t

theorem PFun.mem_core_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (x : α) : x ∈ PFun.core (PFun.res f s) t ↔ x ∈ s → f x ∈ t

theorem PFun.core_res {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) : PFun.core (PFun.res f s) t = sᶜ ∪ f ⁻¹' t

theorem PFun.core_restrict {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : PFun.core (↑f) s = f ⁻¹' s

theorem PFun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.preimage f s ⊆ PFun.core f s

theorem PFun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.preimage f s = PFun.core f s ∩ PFun.Dom f

theorem PFun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.core f s = PFun.preimage f s ∪ (PFun.Dom f)ᶜ

theorem PFun.preimage_asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : PFun.asSubtype f ⁻¹' s = Subtype.val ⁻¹' PFun.preimage f s

def PFun.toSubtype {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β) : α →. Subtype p

Turns a function into a partial function to a subtype.

Equations

• PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }

@[simp]

theorem PFun.dom_toSubtype {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β) : PFun.Dom (PFun.toSubtype p f) = {a : α | p (f a)}

@[simp]

theorem PFun.toSubtype_apply {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β) (a : α) : PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }

theorem PFun.dom_toSubtype_apply_iff {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : α → β} {a : α} : (PFun.toSubtype p f a).Dom ↔ p (f a)

theorem PFun.mem_toSubtype_iff {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : α → β} {a : α} {b : Subtype p} : b ∈ PFun.toSubtype p f a ↔ ↑b = f a

def PFun.id (α : Type u_7) : α →. α

The identity as a partial function

Equations

• PFun.id α = Part.some

@[simp]

theorem PFun.coe_id (α : Type u_7) : ↑id = PFun.id α

@[simp]

theorem PFun.id_apply {α : Type u_1} (a : α) : PFun.id α a = Part.some a

def PFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) : α →. γ

Composition of partial functions as a partial function.

Equations

• PFun.comp f g a = Part.bind (g a) f

@[simp]

theorem PFun.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : α) : PFun.comp f g a = Part.bind (g a) f

@[simp]

theorem PFun.id_comp {α : Type u_1} {β : Type u_2} (f : α →. β) : PFun.comp (PFun.id β) f = f

@[simp]

theorem PFun.comp_id {α : Type u_1} {β : Type u_2} (f : α →. β) : PFun.comp f (PFun.id α) = f

@[simp]

theorem PFun.dom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) : PFun.Dom (PFun.comp f g) = PFun.preimage g (PFun.Dom f)

@[simp]

theorem PFun.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ) : PFun.preimage (PFun.comp f g) s = PFun.preimage g (PFun.preimage f s)

@[simp]

theorem PFun.Part.bind_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : Part α) : Part.bind a (PFun.comp f g) = Part.bind (Part.bind a g) f

@[simp]

theorem PFun.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ →. δ) (g : β →. γ) (h : α →. β) : PFun.comp (PFun.comp f g) h = PFun.comp f (PFun.comp g h)

theorem PFun.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) : ↑(g ∘ f) = PFun.comp ↑g ↑f

def PFun.prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) : α →. β × γ

Product of partial functions.

Equations

• PFun.prodLift f g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun (h : (f x).Dom ∧ (g x).Dom) => ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom)) }

@[simp]

theorem PFun.dom_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) : PFun.Dom (PFun.prodLift f g) = {x : α | (f x).Dom ∧ (g x).Dom}

theorem PFun.get_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) (h : (PFun.prodLift f g x).Dom) : (PFun.prodLift f g x).get h = ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom))

@[simp]

theorem PFun.prodLift_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) : PFun.prodLift f g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun (h : (f x).Dom ∧ (g x).Dom) => ((f x).get (_ : (f x).Dom), (g x).get (_ : (g x).Dom)) }

theorem PFun.mem_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} : y ∈ PFun.prodLift f g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x

def PFun.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) : α × β →. γ × δ

Product of partial functions.

Equations

• PFun.prodMap f g x = { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun (h : (f x.1).Dom ∧ (g x.2).Dom) => ((f x.1).get (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom)) }

@[simp]

theorem PFun.dom_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) : PFun.Dom (PFun.prodMap f g) = {x : α × β | (f x.1).Dom ∧ (g x.2).Dom}

theorem PFun.get_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) (h : (PFun.prodMap f g x).Dom) : (PFun.prodMap f g x).get h = ((f x.1).get (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom))

@[simp]

theorem PFun.prodMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) : PFun.prodMap f g x = { Dom := (f x.1).Dom ∧ (g x.2).Dom, get := fun (h : (f x.1).Dom ∧ (g x.2).Dom) => ((f x.1).get (_ : (f x.1).Dom), (g x.2).get (_ : (g x.2).Dom)) }

theorem PFun.mem_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} : y ∈ PFun.prodMap f g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

@[simp]

theorem PFun.prodLift_fst_comp_snd_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) : PFun.prodLift (PFun.comp f ↑Prod.fst) (PFun.comp g ↑Prod.snd) = PFun.prodMap f g

@[simp]

theorem PFun.prodMap_id_id {α : Type u_1} {β : Type u_2} : PFun.prodMap (PFun.id α) (PFun.id β) = PFun.id (α × β)

@[simp]

theorem PFun.prodMap_comp_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ι : Type u_6} (f₁ : α →. β) (f₂ : β →. γ) (g₁ : δ →. ε) (g₂ : ε →. ι) : PFun.prodMap (PFun.comp f₂ f₁) (PFun.comp g₂ g₁) = PFun.comp (PFun.prodMap f₂ g₂) (PFun.prodMap f₁ g₁)