---

Step * of Lemma subtype_rel-random-variable

∀[k:FinProbSpace]. ∀[n,m:ℕ].  RandomVariable(k;n) ⊆r RandomVariable(k;m) supposing n ≤ m
BY
{ (Unfold `random-variable` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:FinProbSpace].  \mforall{}[n,m:\mBbbN{}].    RandomVariable(k;n)  \msubseteq{}r  RandomVariable(k;m)  supposing  n  \mleq{}  m


By

---

Latex:
(Unfold  `random-variable`  0  THEN  Auto)

---

Home Index