---

Step * of Lemma qavg-same

∀[a:ℚ]. (qavg(a;a) = a ∈ ℚ)
BY
{ ((Unfold `qavg` 0 THEN Auto) THEN QMul ⌜2⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbQ{}].  (qavg(a;a)  =  a)


By

---

Latex:
((Unfold  `qavg`  0  THEN  Auto)  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index