Commit 2023-09-04 13:19 1cf05bbe

View on Github →

feat: More complete lattice WithTop lemmas (#6947) and corresponding lemmas for ℕ∞. Also fix implicitness of iff lemmas.

Estimated changes

added theorem ENat.coe_iInf
modified theorem ENat.coe_iSup
added theorem ENat.coe_sInf
added theorem ENat.coe_sSup
added theorem ENat.iInf_coe_eq_top
added theorem ENat.iInf_coe_lt_top
added theorem ENat.iInf_coe_ne_top
added theorem ENat.iSup_coe_eq_top
modified theorem ENat.iSup_coe_lt_top
added theorem ENat.iSup_coe_ne_top
modified theorem ENNReal.iSup_coe_eq_top
modified theorem ENNReal.iSup_coe_lt_top
added theorem Sigma.exists'
added theorem Sigma.forall'
added theorem iInf_prod'
added theorem iInf_sigma'
added theorem iSup_prod'
added theorem iSup_sigma'
modified theorem WithTop.iSup_coe_eq_top
modified theorem WithTop.iSup_coe_lt_top