Theorems · Theorem · logic and foundations

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

Defined in

Mathlib.Data.PFun

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms