Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
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.
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$.
1 to 4 of 4