Theorems · Theorem · logic and foundations

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

Defined in

Mathlib.Data.PFun

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms