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