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

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

@[simp]

theorem PFun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) : x ∈ f.Dom ↔ ∃ (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 : α →. β) : f.Dom = {x : α | ∃ (y : β), y ∈ f x}

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

Evaluate a partial function

Equations

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

@[simp]

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

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

Evaluate a partial function to return an Option

Equations

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

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

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 : ↑f.Dom) : β

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

Equations

• f.asSubtype s = f.fn ↑s ⋯

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 ∈ f.Dom) : f.asSubtype ⟨x, 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 : α → β) : (↑f).Dom = 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

• f.graph = {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

• f.graph' 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

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

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

• f.restrict H x = Part.restrict (x ∈ p) (f x) ⋯

@[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} (f : α → β) (s : Set α) : α →. β

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

Equations

• PFun.res f s = (↑f).restrict ⋯

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 ∈ 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} (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

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

@[simp]

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

• ⋯ = ⋯

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

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

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

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

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'

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'

def PFun.fixInduction {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {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

• 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 ∈ f.fix a) (H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a') : PFun.fixInduction h H = H a h fun (x : α) (h' : Sum.inr x ∈ f a) => PFun.fixInduction ⋯ H

def PFun.fixInduction' {α : Type u_1} {β : Type u_2} {C : α → Sort u_7} {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

• 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 ∈ 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.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 ∈ 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.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

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

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

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

theorem PFun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : Set α} (h : s ⊆ t) : f.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} (f : α →. β) (s : Set β) : Set α

Preimage of a set under a partial function.

Equations

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

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

@[simp]

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

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

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

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

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 : α →. β) : f.preimage Set.univ = f.Dom

theorem PFun.coe_preimage {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β) : (↑f).preimage 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

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

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

@[simp]

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

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

theorem PFun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s t : Set β} (h : s ⊆ t) : f.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 ∈ s → f 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 β) : f.core s = f.preimage s ∪ f.Domᶜ

theorem PFun.preimage_asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage 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.toSubtype p f).Dom = {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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem PFun.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

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

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

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

Product of partial functions.

Equations

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

@[simp]

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

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

@[simp]

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

theorem PFun.mem_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} : y ∈ f.prodLift 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

• f.prodMap 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 ⋯, (g x.2).get ⋯) }

@[simp]

theorem PFun.dom_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) : (f.prodMap g).Dom = {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 : (f.prodMap g x).Dom) : (f.prodMap g x).get h = ((f x.1).get ⋯, (g x.2).get ⋯)

@[simp]

theorem PFun.prodMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) : f.prodMap 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 ⋯, (g x.2).get ⋯) }

theorem PFun.mem_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} : y ∈ f.prodMap 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 : β →. δ) : (f.comp ↑Prod.fst).prodLift (g.comp ↑Prod.snd) = f.prodMap g

@[simp]

theorem PFun.prodMap_id_id {α : Type u_1} {β : Type u_2} : (PFun.id α).prodMap (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₂ : ε →. ι) : (f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)