# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. Change title to use simple ’ rather than some unicode symbol.

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeAug 11th 2018

Since I had created König’s theorem in the first place: is there something should I have done differently to avoid the unicode symbol problem?

2. Don’t worry about it, it will be from some kind of settings (quite possibly default ones) on your local machine. I will add some handling for it eventually, for now we can just tweak it or add a redirect if we see it.

• CommentRowNumber4.
• CommentAuthorJem Lord
• CommentTime5 days ago

Added a modified version of the theorem that works without choice, essentially by using propositions-as-types to extract the computational content of the original proof. The modified theorem also applies without LEM, but the cardinal inequality structure defined probably isn’t the correct one - if $1 \nsucceq A$ then there is a non-constant map $\Omega \to A$.