Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-25 13:04 a5a98587

View on Github →

feat(data/sigma/basic): cleanup (#3933) Use namespaces Add sigma.ext_iff, psigma.ext and sigma.ext_iff

Estimated changes

modified def psigma.elim
modified theorem psigma.elim_val
added theorem psigma.ext
added theorem psigma.ext_iff
modified def psigma.map
modified theorem psigma.mk.inj_iff
modified theorem sigma.eta
deleted theorem sigma.exists
modified theorem sigma.ext
added theorem sigma.ext_iff
deleted theorem sigma.forall
modified def sigma.map
modified theorem sigma.mk.inj_iff
added theorem sigma.«exists»
added theorem sigma.«forall»