Theorems · Theorem · logic and foundations

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

Defined in

Mathlib.Data.PFun

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms