Commit 2024-10-22 08:37 616d4640

View on Github →

chore(BorelSpace/Order): allow anonymous dot notation on Measurable lemma (#17814) From GibbsMeasure

Estimated changes

added theorem AEMeasurable.biInf
added theorem AEMeasurable.biSup
added theorem Measurable.biInf
added theorem Measurable.biSup
added theorem Measurable.liminf'
added theorem Measurable.liminf
added theorem Measurable.limsup'
added theorem Measurable.limsup
deleted theorem aemeasurable_biInf
deleted theorem aemeasurable_biSup
deleted theorem aemeasurable_iInf
deleted theorem aemeasurable_iSup
deleted theorem measurable_biInf
deleted theorem measurable_biSup
deleted theorem measurable_iInf
deleted theorem measurable_iSup
deleted theorem measurable_liminf'
deleted theorem measurable_liminf
deleted theorem measurable_limsup'
deleted theorem measurable_limsup
deleted theorem measurable_sInf
deleted theorem measurable_sSup