---

Step * of Lemma trans-kernel-increasing

∀rv:InnerProductSpace. ∀e:Point. ∀T:ℝ ⟶ Point ⟶ Point.
  ((e^2 = r1) ⇒ translation-group-fun(rv;e;T) ⇒ (∀h:{h:Point| h ⋅ e = r0} . ∀t,s:ℝ.  ((t < s) ⇒ (ρ(h;t) < ρ(h;s)))))
BY
{ (Auto THEN (FLemma `trans-kernel-is-kernel-fun` [5] THENA Auto) THEN D -1 THEN Reduce -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point.  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point.
    ((e\^{}2  =  r1)
    {}\mRightarrow{}  translation-group-fun(rv;e;T)
    {}\mRightarrow{}  (\mforall{}h:\{h:Point|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t,s:\mBbbR{}.    ((t  <  s)  {}\mRightarrow{}  (\mrho{}(h;t)  <  \mrho{}(h;s)))))


By

---

Latex:
(Auto  THEN  (FLemma  `trans-kernel-is-kernel-fun`  [5]  THENA  Auto)  THEN  D  -1  THEN  Reduce  -1  THEN  Auto)

---

Home Index