---

Step * of Lemma qlog_wf

∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (0 ≤ q) ∧ q < 1} .  (qlog(q;e) ∈ qlog-type(q;e))
BY
{ xxx(Unfold `qlog-type` 0 THEN ProveWfLemma)xxx }

---

Latex:

---

Latex:
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}q:\{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\}  .    (qlog(q;e)  \mmember{}  qlog-type(q;e))


By

---

Latex:
xxx(Unfold  `qlog-type`  0  THEN  ProveWfLemma)xxx

---

Home Index