Step
*
of Lemma
qmin-idempotent
∀[q:ℚ]. (qmin(q;q) = q ∈ ℚ)
BY
{ (Auto THEN Unfold `qmin` 0 THEN SplitOnConclITE THEN Auto) }
Latex:
Latex:
\mforall{}[q:\mBbbQ{}]. (qmin(q;q) = q)
By
Latex:
(Auto THEN Unfold `qmin` 0 THEN SplitOnConclITE THEN Auto)
Home
Index