Commit 2024-09-02 14:29 1672b1b8

View on Github →

feat: Binary version of iSup_eq_top (#16322)

Estimated changes

deleted theorem PSigma.exists'
added theorem PSigma.«exists»
added theorem iInf_psigma'
added theorem iInf_psigma
added theorem iInf₂_eq_bot
added theorem iSup_psigma'
added theorem iSup_psigma
added theorem iSup₂_eq_top