Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-20 11:17 744170a9

View on Github →

feat(data/pfun): Product of partial functions (#15389) Define pfun.prod : (α →. γ) → (β →. δ) → α × β →. γ × δ.

Estimated changes

added theorem pfun.dom_prod_lift
added theorem pfun.dom_prod_map
added theorem pfun.get_prod_lift
added theorem pfun.get_prod_map
added theorem pfun.mem_prod_lift
added theorem pfun.mem_prod_map
added def pfun.prod_lift
added theorem pfun.prod_lift_apply
added def pfun.prod_map
added theorem pfun.prod_map_apply
added theorem pfun.prod_map_id_id