Step
*
of Lemma
rioint_wf
∀[u:ℝ]. ((-∞, u) ∈ Interval)
BY
{ (Unfolds ``rioint interval`` 0 THEN Auto)⋅ }
Latex:
Latex:
\mforall{}[u:\mBbbR{}].  ((-\minfty{},  u)  \mmember{}  Interval)
By
Latex:
(Unfolds  ``rioint  interval``  0  THEN  Auto)\mcdot{}
Home
Index