Lesser limited principle of omniscience

[jkingdon]

This is one of the usual constructive principles between nothing and excluded middle (excluded middle is known as the principle of omniscience because of https://us.metamath.org/ileuni/exmidomni.html ).

We can define/prove:

1. A e. LOmni <-> ∀𝑓 ∈ (2o ↑𝑚 𝐴) ∀g ∈ (2o ↑𝑚 𝐴) ( -. 1o e. ( ran f i^i ran g ) -> ( -. 1o e. ran f \/ -. 1o e. ran g ) ) (see "Stated set-theoretically, the lesser limited principle of omniscience for A" at https://ncatlab.org/nlab/show/principle+of+omniscience#the_lesser_limited_principle_of_omniscience ).
2. analogue to https://us.metamath.org/ileuni/enomni.html for LOmni
3. NN e. LOmni <-> A. f e. ( { 0 , 1 } ^m NN ) ( E* n e. NN ( f ` n ) = 1 -> A. n e. NN ( f ` ( 2 x. n ) ) = 0 \/ A. n e. NN ( f ` ( ( 2 x. n ) + 1 ) ) = 0 ) . This is from https://awswan.github.io/teaching/intuitionisticlogic/lecturenotes/section3.pdf or https://plato.stanford.edu/entries/mathematics-constructive/ (search for "LLPO")
4. A. x e. RR A. y e. RR ( x <_ y \/ y <_ x ) -> _om e. LOmni as described at https://ncatlab.org/nlab/show/principle+of+omniscience#analytic
5. A e. Omni -> A e. LOmni (mentioned at https://ncatlab.org/nlab/show/principle+of+omniscience#analytic at least for A = ω but I suppose maybe true for any A)