search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

Binary logarithm power inequality #4004

Closed metakunt closed 3 months ago

metakunt commented 3 months ago

Thank you @digama0 for your helpful ideas.

tirix commented 3 months ago

I see several new theorems added directly to the main part of set.mm. I think those are fine, but we need to be be fair with @arpie-steele and #3993, so I'd like to hear from others.

metakunt commented 3 months ago

I have moved the theorems back to my mathbox