Metamath Proof Explorer
Table of Contents - 5.4.11. Upper sets of integers
- cuz
- df-uz
- uzval
- uzf
- eluz1
- eluzel2
- eluz2
- eluzmn
- eluz1i
- eluzuzle
- eluzelz
- eluzelre
- eluzelcn
- eluzle
- eluz
- uzid
- uzidd
- uzn0
- uztrn
- uztrn2
- uzneg
- uzssz
- uzssre
- uzss
- uztric
- uz11
- eluzp1m1
- eluzp1l
- eluzp1p1
- eluzaddi
- eluzsubi
- eluzadd
- eluzsub
- subeluzsub
- uzm1
- uznn0sub
- uzin
- uzp1
- nn0uz
- nnuz
- elnnuz
- elnn0uz
- eluz2nn
- eluz4eluz2
- eluz4nn
- eluzge2nn0
- eluz2n0
- uzuzle23
- eluzge3nn
- uz3m2nn
- 1eluzge0
- 2eluzge0
- 2eluzge1
- uznnssnn
- raluz
- raluz2
- rexuz
- rexuz2
- 2rexuz
- peano2uz
- peano2uzs
- peano2uzr
- uzaddcl
- nn0pzuz
- uzind4
- uzind4ALT
- uzind4s
- uzind4s2
- uzind4i
- uzwo
- uzwo2
- nnwo
- nnwof
- nnwos
- indstr
- eluznn0
- eluznn
- eluz2b1
- eluz2gt1
- eluz2b2
- eluz2b3
- uz2m1nn
- 1nuz2
- elnn1uz2
- uz2mulcl
- indstr2
- uzinfi
- nninf
- nn0inf
- infssuzle
- infssuzcl
- ublbneg
- eqreznegel
- supminf
- lbzbi
- zsupss
- suprzcl2
- suprzub
- uzsupss
- nn01to3
- nn0ge2m1nnALT