Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
Order relation on the extended reals
Next ⟩
cltxr
Metamath Proof Explorer
Ascii
Unicode
Table of Contents - 21.20.6.7. Order relation on the extended reals
In this section, we redefine
df-ltxr
without the intermediate step of
df-lt
.
cltxr
df-bj-lt