noncomputable def PFun.ofGraph {α : Type u_1} {β : Type u_2} (g : α → β → Prop) (_hg : ∀ (a : α) (b b' : β), g a b → g a b' → b = b') : α →. β

Equations

• PFun.ofGraph g _hg a = { Dom := ∃ (b : β), g a b, get := fun (h : ∃ (b : β), g a b) => h.choose }

theorem PFun.get_eq {α : Type u_2} {β : Type u_1} {g : α → β → Prop} {hg : ∀ (a : α) (b b' : β), g a b → g a b' → b = b'} (a : α) (b : β) (h : g a b) : (PFun.ofGraph g hg a).get ⋯ = b

@[simp]

theorem PFun.ofGraph_dom {α : Type u_1} {β : Type u_2} {g : α → β → Prop} {hg : ∀ (a : α) (b b' : β), g a b → g a b' → b = b'} : (PFun.ofGraph g hg).Dom = {a : α | ∃ (b : β), g a b}