Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-23 11:58 cc4b8e55

View on Github →

feat(data/sigma,data/ulift,logic/equiv): add missing lemmas (#14903) Add lemmas and equivs about plift, psigma, and pprod.

Estimated changes

added theorem psigma.«exists»
added theorem psigma.«forall»
added theorem plift.down_bijective
added theorem plift.down_surjective
added theorem plift.up_bijective
added theorem plift.up_inj
added theorem plift.up_injective
added theorem plift.up_surjective
added theorem ulift.down_bijective
added theorem ulift.down_surjective
added theorem ulift.up_bijective
added theorem ulift.up_inj
added theorem ulift.up_injective
added theorem ulift.up_surjective