---

Step * 1 of Lemma rlog1


λt.(r1/t) ∈ {f:(r0, ∞) ⟶ℝ| ∀x,y:{a:ℝ| r0 < a} .  ((x = y) ⇒ ((f x) = (f y)))} 
BY
{ ((Assert r0 < r1 BY Auto) THEN MemTypeCD THEN Reduce 0⋅ THEN Auto) }

---

Latex:

---

Latex:

\mlambda{}t.(r1/t)  \mmember{}  \{f:(r0,  \minfty{})  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  r0  <  a\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\} 


By

---

Latex:
((Assert  r0  <  r1  BY  Auto)  THEN  MemTypeCD  THEN  Reduce  0\mcdot{}  THEN  Auto)

---

Home Index