Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Syntax Definition clt 5458

Description: 'Less than' predicate (extended to include the extended reals).

Assertion

Ref	Expression
clt

---

See definition df-ltxr 5462 for more information.

---

Colors of variables: wff set class

Copyright terms: Public domain